Programmé en UVF2R501
Objectifs (obsolète):
Les erreurs dans le fonctionnement des systèmes informatiques peuvent avoir des conséquences graves en termes de vies humaines ou de coûts économiques. Pour éviter ce type de problèmes, l'industrie du logiciel utilise des techniques de validation dont l'application au cours d'un développement mobilise une part importante de l'effort global de réalisation (en moyenne 50% à 60%).
La validation est un processus permettant d'évaluer dans quelle mesure un logiciel satisfait sa spécification. Il repose sur le triptyque :
- description du comportement désiré
- description du comportement effectif
- procédure déterminant le degré de consistance entre ces deux descriptions.
Ce cours présente, dans un esprit ingénierie, une des approches utilisées dans ce domaine : la vérification formelle. A partir d'une base conceptuelle suffisante pour appréhender la problématique de la validation, on procède à des études de cas en utilisant le model-checker SPIN.
Volume horaire :
20h
Contenu détaillé :
Cours 1 : Problématique
Cours 2 : Logiques temporelles
Cours 3 : Model-checking
Cours 4 : Le système SPIN
Cours 5 : Spécification et vérification de protocoles
TP1 : Introduction à SPIN
TP2/TP3 : Etudes de cas
Année 2006/2007
Dernière mise à jour le 12-JUL-06
Validation par le responsable de programme le
| 
