Les lundis, à partir de 14h - UPEC CMC - Salle P2-131

15 mai 2023

AUTOSAR compliant multi-core RTOS formal modeling and verification

Imane Haur (EC Nantes, Sogeti)

La vérification formelle est une solution pour augmenter la fiabilité de l’implémentation du système. Dans ce travail, nous nous intéressons à l’utilisation de ces méthodes pour la vérification des systèmes d’exploitation multi-cœurs temps réel. Nous proposons une approche de model-checking utilisant les réseaux de Petri temporels, étendus avec des transitions colorées et des fonctionnalités de haut niveau. Nous utilisons ce formalisme pour modéliser le système d’exploitation multi-cœur Trampoline, conforme aux standards OSEK et AUTOSAR. Nous définissons dans un premier temps ce formalisme et montrons son adéquation avec la modélisation de systèmes concurrents temps réel. Nous utilisons ensuite ce formalisme pour modéliser le système d’exploitation multi-cœur Trampoline et vérifions par model-checking. À partir de ce modèle, nous pouvons vérifier des propriétés aussi bien sur l’OS que sur l’application  telles que l’ordonnançabilité d’un système temps-réel ainsi que les mécanismes de synchronisation : accès concurrents aux structures de données du système d’exploitation, ordonnancement multi-cœur et traitement des interruptions inter-cœur. À titre d’illustration, cette méthode a permis l’identification automatique de deux erreurs possibles de l’OS Trampoline dans l’exécution concurrente, montrant une protection insuffisante des données et une synchronisation défectueuse.

6 mars 2023

Monitoring cyber-physical systems under uncertainty

Etienne André (LIPN, Université Sorbonne Paris Nord)

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).

13 février 2023

∂ is for Dialectica

Marie Kerjean (LIPN, Université Sorbonne Paris Nord)

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.

30 janvier 2023

Exact reductions of dynamical systems

Gleb Pogudin (LIX)

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.

23 janvier 2023

Exploratory integration of an oracle for mathematical functions in tableau method

François Pessaux (U2IS, ENSTA Paris)

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.

16 janvier 2023

A categorical perspective on context-free grammars and the Chomsky-Schützenberger Theorem

Noam Zeilberger (LIX)

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.

9 janvier 2023

Learning-based control of Cyber-physical systems

Adnane Saoud (CentraleSupelec)

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.

24 octobre 2022

TASTD : Diagrammes états-transitions algébriques temporisés

Marc Frappier

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.

17 octobre 2022

Structures de preuve pour les logiques à point fixe

Luc Pellissier

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

10 octobre 2022

Monte Carlo Tree Search for MDPs: Formal Guarantees and Symbolic Advice

Damien Busatto-Gaston (LACL)

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.