Learning outcomes

  1. Master the concepts for formalising the behaviour of a computer system
  2. Construct algorithms to automatically answer questions (i.e. prove properties) about the behaviour of a computer system
  3. Model real computer system thanks to the above.
 
 
 
 
 

Goals

 
  1. Distinguish differents types of properties: linear, branching, hyperproperties; safety, liveness, fairness properties; regular, context-free.
  2. Understand finite-state automata on infinite words  :
    1. Büchi automata
    2. Rabin automata
    3. Rabin chain automata alias parity automata
 
 
 

Content

Properties, automata, logics, algorithms, specialized data structures.

The projects uses SCADE (ANSYS), and perhaps UPPAAL.

 
 
 

Table of contents

(The numbers refer to the pages of the book of Baier&Katoen)

  1. System Verification 1

  2. Modelling Concurrent Systems 19

  3.   Linear-Time Properties 89

  4. Regular Properties 151

  5. Linear Temporal Logic 229

  6. Computation Tree Logic 313

  7. Timed Automata 673

 

 
 
 
 
 

Assessment method

67% Spoken exam (open book) including exercises 

33% project evaluation

 
 
 
 
 

Sources, references and any support material

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

Anglais