Maitriser la construction de modèles et leurs techniques de vérification.
Le cours théorique couvre les modèles par machines à états, l'expression de propriétés par des machines d'observation, la traduction de logique temporelle en machine d'observation.
A partir de 2017, le travail pratique se réalisé avec l'outil de modélisation formelle SCADE (ANSYS), et, si le temps le permet, l'outil UPPAAL pour les automates temporisés.
System Verification 1
Modelling Concurrent Systems 19
Linear-Time Properties 89
Regular Properties 151
Linear Temporal Logic 229
Computation Tree Logic 313
Timed Automata 673
Cours théorique + exercices en salle + travaux pratiques avec outil.
A partir de 2017, le travail pratique se réalisé avec l'outil de modélisation formelle SCADE (ANSYS), et, si le temps le permet, l'outil UPPAAL pour les automates temporisés.
67% Examen oral à livre ouvert y compris des exercices
33% Evaluation du projet par un rapport (1/3 des points).
Christel Baier, Joost-Pieter Katoen: Principles of Model Checking, The MIT Press (2008).
Principles of the Spin Model Checker by M. Ben-Ari
The SPIN Model Checker: Primer and Reference by Gerard J. Holzmann
Systems and Software Verification: Model-Checking Techniques and Tools by B. Berard, M. Bidoit, A. Finkel, and F. Laroussinie
Model Checking by E. M. Clarke et al.
| Formation | Programme d’études | Bloc | Crédits | Obligatoire |
|---|---|---|---|---|
| Standard | 0 | 5 | ||
| Standard | 0 | 5 | ||
| Standard | 0 | 5 | ||
| Standard | 1 | 5 | ||
| Standard | 2 | 5 | ||
| Standard | 2 | 5 |