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

This is an old revision of the document!


Fondements des systèmes temps-réel et hybrides / Foundations of real time and hybrid systems

Lecturers

Dates

The lectures (5 x 2.5 + 4 x 3 hours) will take place on Thursday (12h45-15h15), in Bat. Sophie Germain, room 1003.

The first lecture is on December 5th 2019.

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 Cachan.

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