Vérification de programmes

Contenu

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).

Modalité d'évaluation

Examen (50%), examen de TP et/ou projets (50%).

Bibliographie

• Livre collectif coordonné par Ph. Schnoebelen : V´erification de logiciels : Techniques et outils du model checking. Vuibert, 1999.
• René David, Karim Nour et Christophe Raffalli, : Introduction à la Logique Théorie de la démonstration, Dunod, 2004
• Yves Bertot, Pierre Castéran : Interactive Theorem Proving and Program Development Coq'Art : The Calculus of Inductive Constructions, Texts in Theoretical Computer Science, An EATCS Series, 2004 96