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.