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.

1. Modélisation
   • Les systèmes de transitions étiquetés
   • La composition parallèle
   • Les réseaux de Petri
2. Spécification
   • Logique temporelle LTL
   • Exemples de propriétés
   • Algorithmes de décision
   • Logique temporelle CTL
   • Exemples et algorithmes
   • Comparaison d'expressivité
3. Utilisation d'outils de model-checking (PRISM, NuSMV,…)

1. Bonne maîtrise de la logique propositionnelle
2. Automates finis
3. Algorithmique dans les graphes