1.    Introduction (3 heures[1])

1.1    Présentation des méthodes formelles; spécifications et vérification de logiciels

1.2    Révision des concepts de base : ensembles, logique et propositions

2.    Langage de spécifications OCL (15 heures)

2.1    Modélisation : UML, MDA, OCL, la notion de contraintes

2.2    Collections, bags, séquences, différence avec Z

2.3    OCL (suite) et sa transcription en code

2.4    Études de cas : Génération de code et discussion

3.    Automates, diagrammes états/transitions, diagrammes d’activités (6 heures)

3.1    Automates et machine: opérations et raisonnements

3.2    Diagrammes états/transitions

3.3    Diagrammes d’activités

4.    Spécifications, analyse et vérification de systèmes concurrents (12 heures)

4.1    AT et RdP : processus, exécution concurrente, objets partagés et exclusion mutuelle

4.2    AT et RdP : propriétés de vivacité et de sécurité, analyses, raisonnement

5.    Autres méthodes et approches - comparaison (3 heures)

5.1    Le langage Z, OCL et Alloy

5.2    UML exécutable

5.3    Vérification de modèles vs techniques de preuve

^[1]   Ces heures sont des heures approximatives d’enseignement pour chaque sujet et incluent le temps alloué à l’examen intra-semestriel.