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.