Aller au contenu

IGL734 - Méthodes formelles de spécification

Présentation

Sommaire

Cycle
2e cycle
Crédits
3 crédits
Faculté ou centre
Faculté des sciences
Répartition de la charge de travail
3-0-6

Cible(s) de formation

Connaitre et comparer les grandes familles de méthodes de spécification formelle (orientées état, orientées évènement, algébriques, hybrides) et les techniques de preuve associées.

Contenu

Bref rappel des outils mathématiques (théorie des ensembles, logique des prédicats du premier ordre, logiques temporelles). Étude de diverses méthodes orientées état, orientées évènement, algébriques et hybrides. Sémantique des langages de spécification formelle (dénotationnelle, opérationnelle, axiomatique, algébrique). Raffinement. Preuve de propriétés. Transformation de spécifications d'une famille à une autre. Génération de tests à partir de spécifications formelles. Étude de prouveurs de théorème.