• produire un modèle abstrait à partir d'une spécification de système rédidigée en langue naturelle;
• valider et interpréter des modèles abstraits réalisés par ses pairs;
• utiliser des outils pour valider et vérifer des modèles;
• rédiger des contraintes et des propriétés en utilisant des langages formels ou semi-formels;
• développer un esprit critique et une sensibilité accrue aux défauts des modèles.

Les 3.5 heures de cours sont interactifs et collaboratifs. Le matériel théorique est rendu disponible à l'avance. Les séances visent à approfondir les notions au travers des exercices pratiques et de courtes présentations magistrales.

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.

1. Projet de spécification en 3 étapes (35%)
2. Projet d'interprétation et de validation (15%)
3. Examen (50%)

• La qualité du français sera prise en considération (jusqu'à 10 % de pénalité).
• La remise de tous les travaux doit respecter les échéanciers fixés. La correction s’effectuant, dans plusieurs cas, le jour même de la remise, tout retard entraîne la note ZÉRO.
• Une participation active des étudiants (es) est exigée. Jusqu’à 5% de la note finale sera retenue pour représenter cette participation. 

la documentation obligatoire sera disponible sur le site Moodle du cours.

Language OCL: WARMER, Jos & KLEPPE, Anneke, The Object Constraint Language Getting your Models Ready for MDA. 2^nd edition, Addison-Wesley, 2003. 

Les sites pertinents seront disponibles sur le site Moodle du cours.