Complex Systems Verification
Nature | UE |
---|
Responsables
Nathalie Bertrand
Objectifs
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ésPré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.Appartient à
Mise à jour le 17 juillet 2017
Contact(s)
Département Informatique
École normale supérieure de RennesCampus de Ker LannAvenue Robert Schuman
35170 BRUZ
Tél. : 02 99 05 52 43
E-mail
Site Internet
École normale supérieure de RennesCampus de Ker LannAvenue Robert Schuman
35170 BRUZ
Tél. : 02 99 05 52 43
Site Internet