IGL734 - Méthodes formelles de spécification

programmes offrant cette activité pédagogique (cours)

Doctorat en informatique

Maîtrise en génie logiciel

Sommaire

Cycle
2e cycle
Crédits
3 crédits
Durée
1 trimestre
Faculté/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.