UE Models and languages for model checking

Degrees incorporating this pedagocial element :

Description

This lecture presents methods and tools for the correct design of systems consisting of agents (or processes) running asynchronously in parallel, possibly subject to real-time constraints. These methods and tools respond to the needs of telecoms (telecommunication protocols), software (distributed algorithms, cloud computing, ...), embedded systems, and hardware (multiprocessor architectures, arbitration protocols, cache coherency protocols, asynchronous circuits, GALS architectures, ...). The methods rely on a formal description of the system in an appropriate language, which can be automatically validated by tools implementing verification techniques, such as model checking or equivalence checking.

Contents :

Basic concepts of asynchronous concurrency and real-time
Formal models: communicating automata, timed automata, process algebras
Formal verification techniques (model checking, equivalence checking)
Temporal logic

Prerequisites

Some knowledge of programming languages.

Bibliography

S. Merz and N. Navet (Eds). Modeling and Verification of Real-Time Systems. Wiley, 2008.