Vérification de modèles
- Code de l'UE INFOM471
-
Horaire
30 15Quadri 1
- Crédits ECTS 5
- Langue
- Professeur Schobbens Pierre-Yves
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.
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.
(The numbers below refer to the pages in the book of Baier&Katoen)
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.
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.
Muhammad Atif, Jan Friso Groote: Understanding Behaviour of Distributed Systems Using mCRL. Springer 2023, ISBN 978-3-031-23007-3
Formation | Programme d’études | Bloc | Crédits | Obligatoire |
---|---|---|---|---|
Master 120 en sciences informatiques, à finalité spécialisée en data science | Standard | 0 | 5 | |
Master 60 en sciences informatiques | Standard | 0 | 5 | |
Master 120 en sciences informatiques, à finalité spécialisée en software engineering | Standard | 0 | 5 | |
Master 60 en sciences informatiques | Standard | 1 | 5 | |
Master 120 en sciences informatiques, à finalité spécialisée en data science | Standard | 2 | 5 | |
Master 120 en sciences informatiques, à finalité spécialisée en software engineering | Standard | 2 | 5 |