Ce cours vise à procurer à l'étudiant ou l'étudiante une connaissance approfondie des méthodes formelles et semi-formelles pour la description et l’analyse de matériels ou de produits logiciels. Il vise également à faire comprendre les avantages et les limites de ces méthodes.

Au terme de ce cours, l'étudiant ou l'étudiante sera en mesure :

• de produire un modèle abstrait et formel d’un système,
• de l’utiliser pour démontrer certaines propriétés
• d'expliquer comment ces propriétés répondent aux spécifications essentielles/critiques du système.

L'étudiant ou l'étudiante devra également être capable de lire et comprendre des spécifications formelles écrites par des professionnels et de produire des spécifications formelles de systèmes de complexité moyenne. Il possèdera une très bonne connaissance des méthodes existantes et saura discuter intelligemment des avantages et des inconvénients de l’utilisation de telles approches.

• 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.