Ensimag Rubrique Formation 2022

Models & languages for model checking - WMM9MO47

  • Number of hours

    • Lectures 18.0
    • Projects -
    • Tutorials -
    • Internship -
    • Laboratory works -
    • Written tests -

    ECTS

    ECTS 3.0

Goal(s)

This lecture is common with the optional lecture 5MMMVSC7 of ENSIMAG 3rd year ISI

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.

Responsible(s)

Frederic LANG

Content(s)

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.

Test

Written examination

Si participation à la SESSION DE RATTRAPAGE, la note finale est la note de l'examen de la SESSION DE RATTRAPAGE.
Sinon, la note finale est la note de l'examen de la SESSION NORMALE.

The exam is given in english only FR

Calendar

The course exists in the following branches:

  • Curriculum - Master 2 in Computer Science - Semester 9 (this course is given in english only EN)
see the course schedule for 2020-2021

Additional Information

Course ID : WMM9MO47
Course language(s): FR

You can find this course among all other courses.

Bibliography

H. Garavel. Défense et illustration des algèbres de processus. In Zoubir Mammeri (Ed), Actes de l'Ecole d'été Temps Réel ETR 2003 (Toulouse, France), Institut de Recherche en Informatique de Toulouse, septembre 2003.
http://www.inrialpes.fr/vasy/Publications/Garavel-03.html

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