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.
-
Prérequis :
Pour suivre ce cours, il faut être familier avec les notions liées aux automates finis et celles vues en cours de logique. Avoir suivi le cours de Théorie et Pratique de la Concurrence en Master 1 est un plus.