COURS/TD de Modélisation et Spécification
M2 Informatique 2020-2021

HORAIRES
ORGANISATION
DESCRIPTIF
Ce cours présente les fondements théoriques pour la spécification et la vérification automatique de systèmes informatiques (programmes, algorithmes, etc).

Pour garantir qu'un système est correct, on peut utiliser des formalismes mathématiques permettant de décrire de manière précise et sans ambiguîté son comportement. De la même façon, on peut aussi se servir de formules logiques pour fournir une spécification précise (c'est-à-dire la description précise des propriétés attendues pour le système étudié).

Nous verrons dans ce cours différents modèles pour caractériser les comportements de systèmes informatiques, comme par exemple les systèmes de transitions étiquetés ou encore les réseaux de Petri, et différentes logiques pour fournir des spécifications formelles, comme par exemple la logique temporelle de temps linéaire LTL ou la logique de temps arborescent CTL.

Nous aborderons également la question des algorithmes permettant de vérifier automatiquement qu'une spécification est valide, que deux systèmes ont le même comportement, ou encore qu' un système respecte une spécification.
MATERIEL MODELISATION
MATERIEL SPECIFICATION
Devoir maison
Enoncé du Devoir Maison à rendre au plus tard le vendredi 27 Novembre 2020 à 23h59!
BIBLIOGRAPHIE