Formal verification is a solution to increase the system’s implementation reliability. In our work, we are interested in using these methods to verify multi-core RTOS. We propose a model-checking approach using time Petri nets extended with colored transitions and high-level features. We use this formalism to model the Trampoline multi-core OS, compliant with the OSEK/VDX and AUTOSAR standards. We first define this formalism and show its suitability for modeling real-time concurrent systems. We then use this formalism to model the Trampoline multi-core RTOS and verify by model-checking its conformity with the AUTOSAR standard. From this model, we can verify properties of both the OS and the application, such as the schedulability of a real-time system and the synchronization mechanisms: concurrent access to the data structures of the OS, multi-core scheduling, and inter-core interrupt handling. As an illustration, this method allowed the automatic identification of two possible errors of the Trampoline OS in concurrent execution, showing insufficient data protection and faulty synchronization.

Monitoring cyber-physical systems attracts both scientific and practical attention. However, monitoring algorithms suffer from the methodological difficulty of only observing sampled discrete-time signals gathered in a log, while real behaviors are continuous-time signals, which implies some uncertainty.
In addition, the monitoring properties can themselves feature some uncertainty: e.g., a period in a property to be monitored can be uncertain or even unknown.
In this presentation, we present two ways to address uncertainty while monitoring cyber-physical systems.

First, we address timed pattern matching in the presence of an uncertain specification. We want to know for which start and end dates in a log, and for what values of the timing parameters, a property holds. For instance, we look for the minimum or maximum period (together with the corresponding start and end dates) for which the property holds.
We rely on two solutions, one based on model-checking, and the other one being ad-hoc.

Second, to mitigate the problem of sampling uncertainties, we introduce a model-bounded monitoring scheme, where we use a (limited) prior knowledge about the target system in order to prune interpolation candidates. We express such prior knowledge by linear hybrid automata (LHAs)—the LHAs are called bounding models. We rely on reachability techniques for linear hybrid automata using polyhedra to efficiently decide whether the property holds on a given log.

We implemented both approaches, and experiments on realistic benchmarks show that both directions are efficient and practically relevant.

This presentation is mainly based on publications at ICECCS 2018 and ACM ToCPS (2022), and are joint work with Masaki Waga (Kyoto University) and Ichiro Hasuo (NII, Tokyo, Japan).

Dialectica is a proof transformation acting of intuitionnistic logic, allowing
the realization of several semi-classical axioms such as Markov’s principle. By
taking the viewpoint of differential lambda-calculus and recent developments in
differentiable programming, we will show how Dialectica computes higher-order
backward differentiation. We will illustrate this through the lens of
categories, types and lambda-terms.

Dynamical systems are frequently used for modeling in the sciences. Building a detailed model often requires taking into account a large number of factors and, as a result, a model may become quite large. High-dimensional models with dozens or hundreds of state variables are not only challenging computationally but it is also hard to use them to derive mechanistic insights. Exact model reduction is a way to address this issue by  finding a self-consistent lower dimensional projection of the corresponding dynamical system. I will describe recent algorithms for computing such reductions and demonstrate them on the models from literature.

The tableaux method is an automated proof search technics initially dealing with first-order logics. Many extensions have been proposed to accommodate different logics and additional theories. Toward the hope to extend this method with guaranteed simulation to prove properties on hybrid systems dynamics described by ODEs, we start with a more modest targe. We present the integration of tableaux to standard arithmetic equations. We show how an oracle can be used to deal with formula involving membership to constant intervals.

I will discuss joint work with Paul-André Melliès in which we analyze context-free grammars as certain kinds of functors of operads, and parsing as a lifting problem [1]. One advantage of this perspective is that it naturally generalizes to enable one to define context-free languages of arrows in any category. Another advantage is that it allows one to study context-free grammars in a common setting with finite state automata, the latter seen as certain kinds of functors of categories. Relying on this (as well as on a surprising adjunction!) we give a categorical reconstruction of (a generalization of) the Chomsky-Schützenberger Representation Theorem, whose classical statement says that any context-free language may be represented as the homomorphic image of the intersection of a Dyck language of balanced parentheses with a regular language.

[1] Parsing as a lifting problem and the Chomsky-Schützenberger representation theorem. MFPS 2022.
https://hal.archives-ouvertes.fr/hal-03702762

In the last few years, learning-based techniques have shown a great success to control complex cyber-physical systems (CPS), where learning-based tools are used either to provide mathematical models of a system, based on which one can synthesize a controller, or to learn directly the controller. However, the use of learning-based techniques in the context of safety critical CPS is particularly problematic, since learning-based components are typically viewed as black box-type systems, lacking formal guarantees. In this talk, we first recall how symbolic control techniques can be used in the context of the control of CPS. In the second part of the talk, we focus on how to provide guarantees when learning is used at the model’s level, namely we show how to learn a symbolic model from data, while providing formal guarantees. This symbolic model will be then used to construct the controller for complex specifications, such as linear temporal logics, based on existing tools in the formal methods community. In the last part of the talk, we focus on the use of learning at the controller’s level. We first use tools from viability theory to develop a general framework for the computation of interval controlled invariants for nonlinear systems. We then show how this framework makes it possible to provide safety guarantees when using neural networks to the control of dynamical systems.

Les diagrammes états-transitions algébriques (Algebraic State-Transition Diagrams (ASTD)) permettent de combiner des machines à états hiérarchiques avec des opérateurs inspirés des algèbres de processus (séquence, choix, garde, fermeture de Kleene, synchronisation, flow, et versions quantifiés de ces opérateurs). Un état d’une machine peut être un ASTD quelconque, ce qui donne une approche entièrement compositionnelle pour la spécifications de systèmes complexes. Des actions pouvant modifier des attributs, d’un type quelconque, déclarés localement dans les ASTD permettent de modéliser les données complexes de manière modulaire.

Nous présenterons une extension temporisée des ASTD, qui permet de spécifier des contraintes temporelles sur le comportement des ASTD. Les nouveaux opérateurs temporels sont: Delay, Persistent Delay, Timeout, Persistent Timeout et Timed Interrupt. Ils sont définis avec deux nouveaux opérateurs ASTD (Persistent Guard et Interruption). Ils peuvent être arbitrairement combinés avec les opérateurs existants. L’extension est basée sur une horloge globale qui fait partie de l’état et qui représente l’horloge système. Un évènement particulièr appelé « step » (inspiré de Stateflow) permet de spécifier des transitions dans les machines à états qui sont déclenchées par l’écoulement du temps. L’évènement step est soumis par l’environnement à un ASTD, typiquement à intervalles réguliers suffisamment petits pour respecter la granularité des contraintes de temps visées.

TASTD est supporté par un éditeur graphique eASTD et un compilateur cASTD qui permet de générer un programme C++ implémentant le comportement spécifié dans un TASTD. Le mode simulation permet d’exécuter le programme généré en contrôlant l’écoulement du temps.

Les preuves avec point-fixes (circulaires et non-bienfondées) permettent d’étudier des logiques exprimant des propriétés co·inductives. Le calcul des séquents présente des difficultés pour exprimer des propriétés indispensables pour la productivité. On présente donc des structures de preuve plus générales.

 

Joint avec Alexis Saurin et Abhishek De

In this talk, we consider the online computation of a strategy that aims at optimizing the expected average reward in a Markov decision process. The strategy is computed with a receding horizon and using Monte Carlo tree search (MCTS), a method known to be scalable to large state spaces. We will present their theoretical guarantees. Formal analysis of MCTS is notably challenging, and we will discuss recent results in that area. Moreover, we augment the MCTS algorithm with a notion of symbolic advice, and show that its theoretical guarantees are maintained. Symbolic advice are used to bias the selection and simulation strategies of MCTS. We illustrate our techniques using a scheduling problem and the popular game Pac-Man.