Model checking [INFOM471]
- 5 credits
- 30h+15h
- 1st quarter
Learning outcomes
- Master the concepts for formalising the behaviour of a computer system
- Construct algorithms to automatically answer questions (i.e. prove properties) about the behaviour of a computer system
- Model real computer system thanks to the above.
Objectives
- Distinguish differents types of properties: linear, branching, hyperproperties; safety, liveness, fairness properties; regular, context-free.
-
Understand finite-state automata on infinite words :
- Büchi automata
- Rabin automata
- Rabin chain automata alias parity automata
Content
The projects uses SCADE (ANSYS), and perhaps UPPAAL.
Table of contents
(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
Teaching methods
Course of lectures ex-cathedra;
Exercises ;
The project will be done with support of the SCADE tool by ANSYS, and perhaps the UPPAAL tool.
Evaluations
67% Spoken exam (open book) including exercises
33% project evaluation
Recommended readings
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
Language of instruction
French / FrançaisLocation for course
NAMUROrganizer
Faculté d'informatiquerue Grandgagnage 21
5000 NAMUR
P. 081725252
F. 081724967
secretariat.info@unamur.be
