Parisian Master of Research in Computer Science
Master Parisien de Recherche en Informatique (MPRI)

Modélisation et vérification des systèmes temporisés / Modélisation and vérification of timed systems

Ce cours a lieu une année sur deux, en alternance avec un cours sur les systèmes temporisés et hybrides.

This lecture takes place once every two years, alternating with a lecture on timed and hybrid systems.

Lecturers

Dates

This course will take during the second semester. Lectures (8 x 3 hours) will take place on Fridays (12:45-15:45), in Bat. Sophie Germain, room 2035.

:!: First lecture on December 10, 2021

The page will be updated as soon as possible.

  • 1st lecture (François Laroussinie): December 10, 2021
  • 2nd lecture (François Laroussinie):
  • 3rd lecture (François Laroussinie):
  • 4th lecture (François Laroussinie):
  • 5th lecture (Patricia Bouyer): January 28, 2022
  • 6th lecture (Patricia Bouyer): February 4, 2022
  • 7th lecture (Patricia Bouyer): February 11, 2022
  • 8th lecture (Patricia Bouyer): February 18, 2022

Les ressources pour la seconde partie du cours se trouvent ici

Basic knowledge in Automata, Logics, Complexity.

While not mandatory, it is useful to know the basics of verification. See for instance the level 1 course 1-22 Basics of verification which can also be taken during M2. Course 1-22 is organized at ENS Paris-Saclay.

Description

[Français] Ce cours s’inscrit dans le domaine de la vérification automatique de programmes. Ici nous mettons l’accent sur les contraintes liées au temps. En général, on parle de contraintes temporelles pour désigner le «temps qualitatif» où on s’intéresse à l’ordre des actions d’un système (ou d’un programme) : «l’alarme doit retentir après le déclenchement d’un problème». Et on parle de contraintes temps-réel (ou temporisées) lorsqu’on s’intéresse aux délais séparant les actions, on parle alors de «temps quantitatif» : «l’alarme doit retentir moins de 10 millisecondes après le déclenchement d’un problème». Dans les deux approches, on cherche à: - modéliser des programmes avec ces contraintes, - spécifier (énoncer) des propriétés portant sur le temps, et - vérifier (avec un algorithme) qu’un modèle vérifie ou non une propriété.

Dans ce cours, nous aborderons ces différents aspects, en commençant par une présentation des logiques temporelles classiques (LTL, CTL, CTL*) pour énoncer des propriétés temporelles. Nous nous intéresserons notamment aux questions d’expressivité et aux algorithmes de décision en lien avec la vérification. Ensuite nous nous intéresserons aux aspects temps-réel en étudiant le modèle des automates temporisés (et de certains systèmes hybrides), puis à des extensions des logiques temporelles pour exprimer des propriétés temps-réel et enfin à des algorithmes d’analyse de ces modèles temporisés.

Nous veillerons à nous concentrer sur les techniques et les problèmes classiques : comment comparer l’expressivité des formalismes étudiés, comment vérifier des systèmes ayant un nombre infini d’états, comment analyser la complexité des problèmes de vérification, etc.

[English] This lecture is part of the domain of automatic verification of programs. We will focus on timing constraints. In general, we speak of temporal constraints, when we only take care of the order of actions: «the alarm should ring after a problem has occurred». We speak of real-time or timed constraints when we are interested in quantitative constraints on delays between actions: «the alarm should ring after a problem has occurred, within 10ms». In these two views, we are interested in: - modelling programs with such constraints, - specifying properties on time, and - verifying (automatically using an algorithm) that a model satisfies a property.

In this lecture, we will study these different aspects. We will start with classical temporal logics (LTL, CTL, CTL*) that are used to express temporal properties. We will in particular be interested in expressiveness questions, and in verification algorithms. Then, we will study real-time aspects and will in particular study the model of timed automata and of some hybrid automata, timed logics and verification algorithms for those models.

We will focus on standard models and technics.

Language

French (or English upon request)

Exam will be available in French (and also in English upon request) and could be written in either French or English.

Related Courses

  • 2-8-1 Non-sequential theory of distributed systems
  • 2-9-1 Mathematical foundations of the theory of infinite transition systems
  • 2-9-2 Algorithmic verification of programs
  • 2-16 Finite automata modelling
  • 2-20-1 Game theory techniques in computer science
  • 2-20-2 Mathematical foundations of automata theory
 
Universités partenaires Université Paris-Diderot
Université Paris-Saclay
ENS Cachan École polytechnique Télécom ParisTech
ENS
Établissements associés Université Pierre-et-Marie-Curie CNRS INRIA CEA