Vérification de programmes

Code UE : SMB212

  • Cours
  • 6 crédits

Responsable national

Pierre COURTIEU

Responsable opérationnel

Pierre COURTIEU

Objectifs pédagogiques

Produire des applications embarquées de confiance en utilisant les méthodes formelles

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 modelchecking 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

Cette UE apparaît dans les diplômes et certificats suivants

Chargement du résultat...
Patientez
Type
Intitulé
Equipe pédagogique
Modalité(s) / Lieu(x)
Code
Intitulé
Equipe pédagogique
Modalité(s) / Lieu(x)
Code
Type Intitulé Equipe pédagogique Modalité(s) / Lieu(x) Code

Contact

Systèmes enfouis et embarqués
2D4P40, 33.1.13, 2 rue Conté
75003 Paris
Tel :01 40 27 26 81
Meriem Bouabdellah

Voir les dates et horaires, les lieux d'enseignement et les modes d'inscription sur les sites internet des centres régionaux qui proposent cette formation

Enseignement non encore programmé