Mon ÉTS  |  Bibliothèque  |  Bottins  |  Emplois  |  Intranet  |  ENGLISH
1er cycle > Fiche de cours
Niveau : 1er cycle
Crédits : 3 cr.
Préalable: MAT210

Charge hebdomadaire :
cours (3 h)
laboratoire (2 h)

Responsable :
Département de génie logiciel et des TI

Fiche de cours

Acquérir des connaissances avancées en modélisation formelle pour l’analyse, la conception et la vérification en génie logiciel. La présentation des concepts couvrant les automates, les langages formels dans un contexte logiciel est complétée par l’étude de trois formalismes couramment utilisés pour modéliser, analyser et vérifier différents types de systèmes.

Distinction entre la spécification de modèles formels et semi-formels. Vérifications par preuves vs vérifications basés sur la génération de modèles. Modélisation : logique du premier ordre, logique modale, logique temporelle (CTL), spécifications UML/OCL, automates temporisés, réseaux de Petri. Analyse des propriétés (déterminisme, non déterminisme, blocage, etc.) et vérification formelle. Interprétation des résultats des vérifications. Application à la vérification et la validation des spécifications logicielles. Brève introduction à la génération automatique du code.

Séances de laboratoire axées sur l’utilisation des outils découlant des méthodes formelles et semi-formelles traitées dans le cours. Spécification d’applications, simulation, validation et vérification formelles avec l’aide d’outils de manière automatique ou semi-automatique.