À la fin du cours, l'étudiant(e) aura assimilé les notions suivantes :

• Niveaux d’abstraction et formalisation

• Différence entre langage formel et semi-formel

• Vérification de modèles

• Avantages et limites des méthodes formelles

• Langage de spécification OCL pour UML

• Spécification avec des diagrammes états/transitions

• Spécifications de systèmes concurrents

• Spécifications de systèmes temps réel

À la fin du cours, l’étudiant(e) sera capable de :

• Lire des spécifications formelles écrites dans un langage proche de la logique du premier ordre;

• Écrire des spécifications formelles dans un langage proche de la logique du premier ordre;

• Comprendre des spécifications formelles écrites par des professionnels;

• Spécifier un modèle UML avec OCL;

• Spécifier un modèle simple d’un système concurrent;

• Vérifier avec l’aide d’outils ses modèles UML/OCL;

• Analyser les résultats de ses vérifications.

• 3.5 heures de cours et 2 heures de laboratoire par semaine. Certains documents pertinents au cours (mémos, exercices, solutionnaires, énoncés de travaux, fichiers d'exemples, etc.) seront placés régulièrement sur le site WEB du cours. Il est de la responsabilité de l'étudiant de consulter régulièrement ce site.

• Les laboratoires visent l'assimilation des notions vues au cours et la mise au point des travaux pratiques.