Objectifs de l'enseignement

Présenter la vérification formelle de systèmes répartis à l'aide des outils de base à savoir les réseaux de Petri, les automates... puis voir les logiques temporelles LTL et CTL et enfin développer les algorithmes de vérification basés sur le model-checking.

 

Plan du cours

• Les réseaux de Petri TD
• Les automates TD
• Logiques temporelles TD
• model-checking TD
• méthodes de réduction
• Notes de Cours
• Examen juin 2009
• Examen de Rattrapage 2009

 

Bibliographie

• E.M.Clarcke, O.Grumberg, D.A.Peled, Model Checking 1999
• M.Diaz, Vérification et mise en oeuvre des réseaux de Petri. Lavoisier 2003
• C.A.R Hoare, "communicating sequential processes" deux communications of the ACM vol 21 n°8 1978 p 666 - 677
• Annie Choquet-Geniet, Les réseaux de Petri un outil de modélisation - DUNOD.