Candidater
Brochures
Prendre RDV
Voir l’agendaLa recherche en théorie des automates et vérification à l’EPITA
Comment vérifier qu’un logiciel respecte les règles prévues, même dans des situations difficiles à anticiper ? À l’EPITA, la théorie des automates permet de représenter et d’analyser les comportements des systèmes informatiques. Avec le logiciel libre Spot, les chercheurs développent des méthodes de vérification pour détecter des erreurs et contribuer à la fiabilité des logiciels et des protocoles, et des méthodes de synthèse pour construire automatiquement un système respectant des spécifications formelles
Comprendre la recherche en vérification formelle avec les experts de l’EPITA
Des questions ? Venez nous les poser !
À Paris, Lyon, Rennes, Strasbourg ou à Toulouse, venez rencontrer nos étudiantes et étudiants et échanger avec eux sur la vie étudiante à l’EPITA.
Les enjeux de la recherche en théorie des automates à l’EPITA
Un logiciel ou un protocole peut suivre de nombreux chemins selon les événements qu’il rencontre. Les chercheurs de l’EPITA étudient comment représenter ces possibilités, définir les règles à respecter et rechercher les comportements qui les enfreignent. La vérification formelle associe ainsi précision mathématique et efficacité des algorithmes.
Modéliser les comportements des systèmes dans la durée
Un automate fini possède un nombre limité d’états. Il peut notamment reconnaître des suites de symboles, appelées mots, et déterminer leur appartenance à un langage formel. Ces notions permettent de décrire des séquences et les règles qui les organisent.
À l’EPITA, les recherches portent notamment sur les omega-automates, qui reconnaissent des séquences infinies. Ils permettent de raisonner sur des systèmes dont le fonctionnement peut se poursuivre indéfiniment, comme un protocole qui échange continuellement des messages. L’enjeu est de représenter ces comportements sous une forme exploitable par les algorithmes de vérification.
Exprimer précisément les propriétés à vérifier
Avant de vérifier un système, il faut définir ce que l’on attend de lui. Une requête doit-elle toujours recevoir une réponse ? Une situation interdite peut-elle survenir ? Les logiques temporelles permettent de formuler ces exigences en tenant compte de l’ordre et de l’évolution des événements.
Les chercheurs de l’EPITA étudient notamment la traduction de ces formules en automates. Cette étape relie une propriété exprimée mathématiquement aux méthodes qui permettront de l’analyser. La conclusion obtenue porte sur cette propriété et sur le modèle étudié : elle dépend donc aussi de la manière dont le système a été représenté.
Vérifier des modèles toujours plus complexes
Lorsque plusieurs composants interagissent, le nombre de configurations possibles peut augmenter très rapidement. Cette explosion de l’espace d’états rend la vérification coûteuse en temps de calcul et en mémoire.
Les recherches de l’EPITA visent à améliorer la représentation et l’exploration de ces configurations. Le model checking, ou vérification de modèles, cherche à établir si les comportements du modèle respectent les propriétés définies. Lorsqu’une propriété est violée, un contre-exemple peut montrer la succession d’événements qui conduit au problème et aider à comprendre l’erreur.
Les projets et travaux de recherche en automates à l’EPITA
Les travaux de l’équipe Automates et Applications associent conception d’algorithmes, développement logiciel et collaborations scientifiques. Spot permet de diffuser des méthodes de manipulation d’automates et de logique temporelle. Le projet TiCKTaC a exploré les contraintes des systèmes temps réel, tandis que les recherches sur l’apprentissage de modèles étudient comment construire des représentations à partir d’observations.
Spot : développer des outils pour la vérification et la synthèse de contrôleurs
Développé par l’équipe Automates et Applications, Spot est un logiciel libre consacré à la manipulation d’omega-automates et de formules de logique temporelle. Il rassemble des algorithmes pour traduire, transformer et simplifier ces objets, afin de les utiliser dans des démarches de vérification.
Spot contribue également à la synthèse automatique de contrôleurs. Il s’agit de construire automatiquement, à partir d’exigences formelles, une système réagissant aux événements de son environnement en respectant respecter ces exigences.
La diffusion du logiciel permet à d’autres chercheurs d’utiliser les méthodes développées, de les comparer et de construire de nouveaux outils à partir de ces travaux. Elle relie ainsi les avancées théoriques à des moyens d’expérimentation accessibles à la communauté scientifique.
TiCKTaC : prendre en compte les contraintes des systèmes temps réel
Dans un système temps réel, le moment où une action se produit compte autant que l’action elle-même. La vérification doit donc tenir compte de contraintes de durée et de délais.
L’équipe Automates et Applications a participé au projet TiCKTaC , financé par l’Agence nationale de la recherche et mené de 2019 à 2023. Les travaux ont porté sur la vérification et la synthèse de systèmes temps réel à l’aide d’automates temporisés, qui intègrent des horloges pour représenter ces contraintes.
Le projet a contribué au développement de TChecker, un outil libre de vérification. Les méthodes ont notamment été étudiées sur des cas de planification robotique et d’analyse de performances de réseaux ferroviaires.
Apprendre des modèles à partir de comportements observés
Comment construire une représentation d’un système à partir de ce que l’on observe de son fonctionnement ? Les travaux de l’équipe sur le raisonnement automatisé explorent notamment l’apprentissage de modèles : produire des automates ou des formules logiques à partir d’ensembles de séquences d’événements.
Ces recherches rejoignent des questions d’apprentissage et d’explicabilité également centrales en intelligence artificielle. Il peut s’agir, par exemple, de trouver une formule temporelle qui distingue deux ensembles de comportements observés. Cette formule fournit alors une règle explicite pour comprendre ce qui les différencie.
L’équipe étudie plusieurs méthodes pour construire ces représentations, notamment à partir d’exemples disponibles ou d’interactions permettant d’obtenir de nouvelles informations sur le système.
Comment la recherche en théorie des automates nourrit-elle la formation à l’EPITA ?
Les recherches en théorie des automates donnent une application concrète aux liens entre modèles mathématiques, algorithmes et programmation. Elles montrent comment une question de fiabilité devient un problème scientifique, puis un développement logiciel. À l’EPITA, cet environnement permet aussi à des étudiants de découvrir la recherche à travers des contributions aux outils du laboratoire.
En cycle ingénieur, développer une démarche d’analyse des systèmes
Le cycle ingénieur de l’EPITA associe formation scientifique, développement informatique et projets. Les recherches sur les automates éclairent une démarche essentielle pour concevoir des systèmes : préciser un comportement attendu, choisir une représentation adaptée et examiner les limites d’une méthode.
Le cursus propose également des dispositifs d’exposition à la recherche et une mineure Recherche. Ils permettent aux étudiants intéressés par les questions scientifiques d’approfondir cette dimension de leur formation, en complément de leur spécialisation technique.
Découvrir le cycle ingénieurContribuer à un logiciel de recherche comme Spot
Dans sa présentation des travaux sur le model checking à l’EPITA , Alexandre Duret-Lutz décrit la contribution d’un étudiant à l’amélioration d’un algorithme de réduction d’automates intégré à Spot.
Ce type de projet conduit à lire des publications scientifiques, comprendre une méthode et chercher à l’implémenter efficacement. Les étudiants impliqués découvrent ainsi comment la programmation contribue à faire avancer une question de recherche, au contact des enseignants-chercheurs.
Téléchargez la brochure !
Enseignements, modules, projets étudiants, vie associative… Découvrez la documentation EPITA !
