Master Parisien de Recherche en Informatique

Fondements pour la vérification des systèmes temps-réel (48h, 6 ECTS)

Cours 2009-2010 : Intervenants

Horaires du cours :

Langues du cours :

Les étudiants seront autorisés à rédiger leur examen en français ou anglais.

Supports de cours :

Pré-requis :

Motivations et objectifs du cours

Les systèmes informatiques sont de plus en plus répandus (dans les téléphones, les véhicules automobiles, etc.), de plus en plus complexes, et ont très souvent un rôle critique (avions, centrales nucléaires, etc.). Pour ces raisons, la vérification de ce genre de systèmes s'est largement développé ces dernières années.

Plusieurs techniques permettent de s'assurer du bon comportement d'un système informatique. L'approche "naïve", qui consiste à construire puis tester le système, est souvent un passage obligé (comme en attestent les nombreux essais de l'Airbus A380), mais elle n'est généralement pas exhaustive. Les méthodes formelles, basées sur des raisonnements mathématiques, sont donc souvent préférées au moment de la conception des systèmes. L'approche retenue dans ce cours est le model-checking. Elle consiste à modéliser le comportement du système à vérifier, à énoncer formellement les propriétés de correction attendue puis à appliquer des algorithmes pour décider si le modèle satisfait la propriété.

Cette approche nécessite le développement d'outils mathématiques adaptés. D'une part, il faut pouvoir représenter le comportement du système : on peut pour cela utiliser des automates, des algèbres de processus, etc. D'autre part, il faut disposer de langages formelles pour énoncer des propriétés complexes : on peut par exemple utiliser des logiques temporelles, qui permettent de spécifier des propriétés sur l'ordonnancement des actions du système... Enfin le développement d'algorithmes de model-checking (afin de vérifier automatiquement et de manière exhaustive que tous les comportements de l'automate satisfont la propriété) nécessite des techniques très fines pour faire face aux problèmes de complexité.

Dans ce cours, nous présenterons le cadre général de la vérification par model-checking pour les systèmes temps-réel, ainsi que plusieurs extensions classiques (hybrides, probabilistes).

Description du cours

1. Automates temporisés et hybrides [18h] (Eugène Asarin)
2. Automates pondérés [15h] (Benedikt Bollig)
3. Systèmes temporisés probailistes [15h] (Serge Haddad)

Description détaillée

Partie I : Automates temporisés et hybrides

Intervenant : Eugene Asarin.

Partie II : Automates pondérés

Intervenant : Benedikt Bollig.

Partie III : Systèmes temporisés probabilistes

Intervenant : Serge Haddad.

Bibliographie générale

• Principles of Model Checking. C. Baier, J.P. Katoen. MIT Press, 2008.
• Reactive Systems: Modelling, Specification and Verification. L. Aceto, A. Ingólfsdóttir, K.G. Larsen, J. Srba. Cambridge Univ. Press, 2007.
• Model Checking. E.M. Clarke, O. Grumberg, D.A. Peled. MIT Press, 1999.
• Systems and Software Verification. Model-Checking Techniques and Tools. B. Bérard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, and Ph. Schnoebelen. Springer, 2001.
• The Temporal Logic of Reactive and Concurrent Systems: Specification. Z. Manna and A. Pnueli. Springer, 1991.
• Temporal Verification of Reactive Systems: Safety. Z. Manna and A. Pnueli. Springer, 1995.

Les années précédentes

• Année 2008-2009
• Année 2007-2008
• Année 2006-2007

Équipe pédagogique