Description
Date depot: 29 septembre 2021
Titre: Traduction à la volée de logiques temporelles industrielles en ω-automates
Directeur de thèse:
Alexandre DURET-LUTZ (LRE)
Encadrant :
Etienne RENAULT (LRE)
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Modèles de calcul, preuve, vérification
Resumé: Différentes techniques de vérification formelle utilisent des formules
de logique temporelle, telle que la logique temporelle à temps
linéaire (LTL), pour spécifier des comportements attendus. De telles
formules sont ensuite traduites sous forme d'ω-automates, typiquement
des automates de Büchi, avant de réaliser un processus de
vérification.
Les applications d'une telle transformation sont nombreuses: model
checking, synthèse de contrôleur, génération de tests, etc.
L'objectif de ce projet est de s'intéresser, non pas à la logique LTL,
mais à des logiques plus expressives : LDL (linear dynamic logic), PSL
(property specification language), et SVA (SystemVerilog Assertions).
Ces deux dernières logiques sont des standards industriels. Dans les
trois cas, la logique est augmentée avec des expressions régulières,
et parfois des opérateurs temporels faisant intervenir le passé.
Doctorant.e: Martin Antoine Yves