Vérification de programmes
6 crédits Pierre COURTIEU EPN05 - Informatique Unité d'enseignement de type cours
Publié Du 01-09-2011 au 31-08-2019
Produire des applications embarquées de confiance en utilisant les méthodes formelles
L'unité SMB212 apparaît dans 1 cursus.
Il est reconnu que la conception d'applications à haut degré de fiabilité et de sécurité nécessite l'apport des méthodes formelles. Ce cours vise à donner une base théorique et formelle solide sur les aspects nécessaires à la vérification des systèmes embarqués, en particulier la preuve, le model checking et le test. Les thèmes abordés concernent les spécifications formelles, la preuve, la vérification de modèles par model-checking, et la génération de test guidée par les propriétés. L'accent sera mis également sur la mise en oeuvre de ces techniques pour détecter des failles de sûreté et/ou de sécurité avec des outils tels que l'atelier Focal, l'assistant à la preuve Coq et SPIN associé à Coloane et framekit (du LIP6 : outils génériques qui se greffent au dessus de spin et autres).
Examen (50%), examen de TP et/ou projets (50%).
| Titre | Auteur(s) |
|---|---|
| V´erification de logiciels : Techniques et outils du model checking. Vuibert, 1999. | Livre collectif coordonné par Ph. Schnoebelen |
| Introduction à la Logique Théorie de la démonstration, Dunod, 2004 | René David, Karim Nour et Christophe Raffalli, |
| Interactive Theorem Proving and Program Development CoqArt : The Calculus of Inductive Constructions, Texts in Theoretical Computer Science, An EATCS Series, 2004 96 | Yves Bertot, Pierre Castéran |