Vérification de Systèmes Complexes (CSV)

Description

La vérification, ou model-checking, permet de prouver automatiquement qu’un modèle d’un système satisfait une propriété donnée. Ce module aborde des techniques de vérification pour des systèmes complexes. On s’intéressera en particulier à des modèles à espace d’état infini. Considérer de tels modèles est naturel dans plusieurs situations : par exemple en présence d’une structure de données a priori non bornée, comme une file de communication, ou une pile d’appels ; mais aussi comme représentation d’un domaine dense comme le temps continu ; ou encore pour traiter uniformément une famille de systèmes indexés par un paramètre pouvant prendre une valeur arbitraire. Ce cours présentera quelques classes de modèles complexes ainsi que des techniques de vérification associées.

Mots-clés

Vérification ; model checking ; automates ; réseaux paramétrés

Prérequis

Connaissances solides en automates finis; algorithmique des graphes; complexité. Suivre en parallèle, ou avoir suivi un module de model checking pour les systèmes finis sera un plus indéniable. Le module MAD sur la vérification et l'algorithmique des systèmes distribués est complémentaire.

Contenu

Dans une première partie, on s’intéressa programmes récursifs ou les systèmes temps-réels. On introduira pour chacun un modèle naturel : les automates à pile, et les automates temporisés, respectivement. On présentera ensuite des abstractions adaptées pour la vérification de ces systèmes. Dans une deuxième partie, on s’intéressera à des systèmes distribués dans lesquels le nombre de processus est soit variable, soit inconnu, et les processus ne portent pas d’identifiants. On introduira quelques modèles pour ce type de systèmes (protocoles de diffusion, protocoles de population, réseaux ad hoc paramétrés) et des algorithmes de vérification correspondants.

Compétences acquises

Ce module permettra aux étudiant.e.s de maîtriser les techniques de vérification pour les systèmes complexes. Il offrira un panorama des outils utilisés en model checking.

Enseignants

Nathalie Bertrand (responsable), Nicolas Markey