Application de la théorie des automates, le développement d’algorithmes performants pour le Model Checking doit permettre de garantir la qualité de fonctionnement de tous les nouveaux systèmes complexes.
Des thématiques d’excellence
- L’algorithmique des omega-automates
Ces automates sont des structures de données permettant de représenter et raisonner sur des ensembles infinis de comportements infinis. - Les logiques temporelles
Les formules de ces logiques sont utilisées pour spécifier des comportements désirables ou indésirables. Elles utilisent différents modèles d’écoulement du temps pour imposer des contraintes entre des événements survenant à différents instants.
Recherche en cours, zoom sur le Model Checking
Garantir la sureté d’un système de façon automatique
Les automates sont des structures de données qui peuvent être utilisées pour modéliser l’ensemble de comportements possibles d’un système physique, d’un programme, ou encore d’un protocole. Ces modèles permettent d’écrire des algorithmes qui vérifient automatiquement et de façon exhaustive tous les comportements possibles du système : c’est le model checking.
Lorsqu’un outil de model checking trouve une erreur, il montre un exemple de comportement anormal du système, et permet ainsi sa correction. Des enseignants-chercheurs de l’équipe de recherche Automates et Applications travaillent à améliorer les techniques de model checking, qu’ils distribuent sous la forme d’un logiciel libre.
Des collaborations pointues
- Laboratoire d’informatique de Paris 6 (Sorbonne Université).
- Faculty of Informatics, Masaryk University (Brno, République Tchèque).
De grands projets
- Spot logiciel libre pour la manipulation efficace d’automates et de formules de logique temporelle.
Applications possibles au model checking (vérification automatique de propriétés comportementales sur des modèles) ou à la synthèse automatique de contrôleurs satisfaisant des spécifications. - Participation au projet TickTac financé par l’ANR : développement d’outils pour la vérification et la synthèse de systèmes temps-réels.