Ce cours aborde d'une part la construction de modèles formels pour la description du comportement des systèmes informatiques et d'autre part la construction de spécifications (les propriétés attendues) de ces systèmes.
Syllabus
Sujets centraux
Modélisation
Les systèmes de transitions étiquetés
La composition parallèle
Les réseaux de Petri
Spécification
Logique temporelle LTL
Exemples de propriétés
Algorithmes de décision
Logique temporelle CTL
Exemples et algorithmes
Comparaison d'expressivité
Utilisation d'outils de model-checking (PRISM, NuSMV,…)