Ma thèse s'intèresse à la compilation vérifiée de machines à états hierarchiques dans un langage synchrone à flots de données inspiré de Scade 6. Vous pouvez trouver mon manuscript ici et les transparents de ma soutenance ici.
My thesis focuses on the verified compilation of hierarchical state machines in a synchronous dataflow language inspired by Scade 6. You can find my manuscript here and the slides of my defense here.
Ma soutenance de thèse aura lieu le 13 octobre 2023 à 13h30 (heure de Paris). La soutenance aura lieu à l'ENS, au 45 rue d'Ulm, 75005 Paris. La présentation sera en anglais. Il y aura bien sûr un pot après la soutenance !
The defense will take place on october 13 2023 at 13:30 (Paris time). It will take place in ENS, 45 rue d'Ulm, 75005 Paris. The defense will be in english.
| RapporteurReviewer | Magnus Myreen | Chalmers University of Technology |
| RapporteurReviewer | Robert de Simone | Inria |
| PrésidentePresident | Florence Maraninchi | Université Grenoble Alpes |
| ExaminateurExaminer | Carlos Agon | IRCAM |
| ExaminateurExaminer | Julien Forget | Université de Lille |
| ExaminateurExaminer | Xavier Leroy | Collège de France |
| Co-directeurCo-director | Timothy Bourke | Inria / ENS |
| Co-directeurCo-director | Marc Pouzet | ENS / Inria |
La soutenance aura lieu dans la salle W qui se trouve au 4e étage du batiment Rataud. Un plan d'accès est dessiné sur l'invitation. Pour accéder à la salle, entrez au 43 rue d'Ulm. Entrez ensuite par la grande porte. Avancez tout droit pour traverser le hall, la cour aux Ernest et le couloir arrière du batiment. Tournez à droite, et avancez tout droit jusqu'au fond de la cour Pasteur. Entrez dans le batiment Rataud par la porte à votre gauche, et montez en ascenceur jusqu'au 3e étage. Prenez ensuite les escalier à droite jusqu'au 4e. Suivez ensuite le couleur qui va tout droit, puis à gauche. Vous devriez avoir une belle vue de Paris, puis arriver devant la salle.
La soutenance sera également retransmise en ligne. Vous pouvez la suivre sur https://bbb.di.ens.psl.eu/b/bas-cnb-1wl-vii.
The defense will take place in salle W on the 4th floor of the Rataud building. An access map is presened on the invitation. To access the room, enter by 43 rue d'Ulm. Cross the big door to the main building. Go straight through the hall, the central patio, and the back corridor. Once outside again, tourn right, and go straight to the back of cour Pasteur. Enter the Rataud building on the left, and take the lift to the 3rd floor. Then, take the stairs to the 4th. Follow the corridor ahead, and then right. You should have a nice view of Paris, then arrive in from of salle W.
The defense will also be transmitted online. Yon can follow it at https://bbb.di.ens.psl.eu/b/bas-cnb-1wl-vii.
Les systèmes embarqués critiques sont souvent spécifiés par des
formalismes schéma-bloc. SCADE Suite est un environnement de
développement pour ces systèmes utilisé depuis vingt ans dans
l'industrie avionique, nucléaire, automobile, et autres domaines
critiques. Son formalisme graphique se traduit en une
représentation textuelle basée sur le langage synchrone à flots de
données Lustre, et incorpore des fonctionnalités de langages plus
récents comme Lucid Synchrone. En Lustre, un programme est défini
comme un ensemble d'équations qui spécifie la relation entre
entrées et sorties du programme à chaque instant. Le langage des
expressions inclut des opérateurs arithmétiques et logiques, des
opérateurs de délais qui permettent d'accéder à la précédente
valeur d'une expression, et des opérateurs d'échantillonage qui
permettent à certaines valeurs d'être calculées moins souvent que
d'autres.
Le projet Vélus est une formalisation d'un
sous-ensemble du langage Scade 6 dans l'assistant de preuves Coq.
Il propose une formalisation de la sémantique dynamique du langage
sous forme de relations entre flots infinis d'entrées et de
sorties. Il inclut aussi un compilateur qui utilise CompCert, un
compilateur vérifié pour C, pour produire du code assembleur.
Enfin, il fournit une preuve de bout-en-bout que ce compilateur
préserve la sémantique à flots de données des programmes sources.
Cette thèse étends Vélus en y ajoutant les blocs de
contrôles de Scade 6 et Lucid Synchrone, ce qui inclut une
construction qui contrôle l'activation des équations selon une
condition (switch), une construction permettant d'accéder à la
valeur précédente d'une variable (last), une construction qui
réinitialise les opérateurs de délai (reset), et, enfin, des
machines à états hiérarchiques, qui permettent la spécification de
comportements modaux complexes. Toutes ces constructions peuvent
être arbitrairement imbriquées dans un programme. Nous étendons la
sémantique de Vélus avec une nouvelle spécification pour ces
constructions qui encode leur comportement par l'échantillonnage.
Nous proposons un schéma d'induction générique pour les programmes
bien formés qui permet de prouver certaines propriétés du modèle
sémantique, comme son déterminisme ou l'adhérence des valeurs aux
types déclarés. Enfin, nous décrivons la compilation de ces
constructions telle qu'implémentée dans Vélus. Nous montrons que
le modèle de compilation qui réécrit ces constructions dans le
langage noyau peut être implémenté, spécifié et vérifié dans Coq.
La compilation de last et reset nécessite des changements plus
profonds dans les langages intermédiaires de Vélus.
Safety-critical embedded systems are often specified using
block-diagram formalisms. SCADE Suite is a development environment for
such systems which has been used industrially in avionics, nuclear
plants, automotive and other safety-critical contexts for twenty
years. Its graphical formalism translates to a textual representation
based on the Lustre synchronous dataflow language, with extensions
from later languages like Lucid Synchrone. In Lustre, a program is
defined as a set of equations that relate inputs and outputs of the
program at each discrete time step. The language of expressions at
right of equations includes arithmetic and logic operators, delay
operators that access the previous value of an expression, and
sampling operators that allow some values to be calculated less often
than others.
The Vélus project aims at formalizing a subset of the Scade 6 language
in the Coq Proof Assistant. It proposes a specification of the dynamic
semantics of the language as a relation between infinite streams of
inputs and outputs. It also includes a compiler that uses CompCert, a
verified compiler for C, as its back end to produce assembly code, and
an end-to-end proof that compilation preserves the semantics of
dataflow programs.
In this thesis, we extend Vélus to support control blocks present in
Scade 6 and Lucid Synchrone, which includes a construction that
controls the activation of equations based on a condition (switch), a
construction that accesses the previous value of a named variable
(last), a construction that re-initializes delay operators (reset),
and finally, hierarchical state machines, which allow for the
definition of complex modal behaviors. All of these constructions may
be arbitrarily nested in a program. We extend the existing semantics
of Vélus with a novel specification for these constructs that encodes
their behavior using sampling. We propose a generic induction
principle for well-formed programs, which is used to prove properties
of the semantic model such as determinism and type system correctness.
Finally, we describe the extension of the Vélus compiler to handle
these new constructs. We show that the existing compilation scheme
that lowers these constructs into the core dataflow language can be
implemented, specified and verified in Coq. Compiling the reset and
last constructs requires deeper changes in the intermediate languages
of Vélus.