Model checking
- UE code INFOM471
-
Schedule
30 15Quarter 1
- ECTS Credits 5
-
Language
English
- Teacher
The projects uses SCADE (ANSYS), and perhaps UPPAAL.
(The numbers refer to the pages of the book of Baier&Katoen)
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
67% Spoken exam (open book) including exercises
33% project evaluation
Main reference book: Christel Baier, Joost-Pieter Katoen: Principles of Model Checking, The MIT Press (May 31, 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
Training | Study programme | Block | Credits | Mandatory |
---|---|---|---|---|
Master 120 en sciences informatiques, à finalité spécialisée en software engineering | Standard | 0 | 5 | |
Master 60 en sciences informatiques | Standard | 0 | 5 | |
Master 120 en sciences informatiques, à finalité spécialisée en data science | 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 |