Introduction à la vérification
Responsable : Anca Muscholl et Marc Zeitoun
Ce cours du S8 est uniquement pour le parcours IF. Il vaut 6 ECTS.
Résumé
Le cours introduit des techniques de vérification automatique, en particulier le model-checking pour différentes sortes de systèmes : systèmes finis, automates communicants, automates temporisés, réseaux de Petri, systèmes à compteurs. On introduit plusieurs formalismes logiques permettant d'exprimer des spécifications de tels systèmes, en particulier les logiques temporelles LTL, CTL et CTL*. Le cours présente des algorithmes permettant de vérifier automatiquement qu'un tel système vérifie une propriété exprimée dans un de ces formalismes, quand c'est possible. Une partie du cours consiste à manipuler le model-checker SPIN, en modélisant des protocoles et en vérifiant s'ils satisfont des propriétés.
Le contrôle continu pourra prendre plusieurs formes, au choix : implémentation d'algorithmes vus en cours, vérification de propriétés de protocoles à modéliser en SPIN, lecture d'articles.