Logiciels sûrs
Développement de logiciels sûrs
Description : Ce cours permettra aux étudiants de découvrir les concepts de base de la méthode formelle Event-B à travers les activités de modélisations et de la preuve en utilisant l’Atelier Rodin, l’IDE principal de la méthode Event-B. L’application d’une approche de spécification Top-Down permettra aux étudiants d’utiliser le raffinement, qui est l’une des opérations de base de la méthode Event-B, et de générer automatiquement un code C vérifié et conforme à la spécification initiale. L’animation de modèles Event-B en utilisant l’outils ProB est également abordée. Enfin, pour couvrir les besoins de vérification d’un code critique existant, les techniques de vérification formelle seront également présentées et mises en pratique avec les greffons WP et MetAcsl de la plateforme Frama-C.
Acquis d’apprentissage : À la fin de ce cours, les étudiants seront capable d’appliquer un processus de développement de logiciels critiques complet en partant de la spécification jusqu’à la génération automatique du code source.
Modalités d’évaluation : Evaluation à partir des participations aux manipulations (TD/TP) et des résultats rendus
Compétences évaluées :
- Développement
- Certification
Responsable de cours : Idir Ait Sadoune
Identifiant Geode : SPM-INF-023
CM :
- Introduction à la méthode Event-B (1.5 h)
- L’activité de preuve dans la méthode Event-B (1.5 h)
- Le raffinement d’un modèle Event-B (1.5 h)
- Introduction au Model-Checking (1.5 h)
- Validation d’une spécification Event-B par Model-Checking (1.5 h)
- Spécification et vérification formelle avec Frama-C/WP (3.0 h)
- Vérification formelle de propriété de sécurité avec Frama-C/MetAcsl (3.0 h)
TD :
- Introduction à la méthode Event-B (1.5 h)
- L’activité de preuve dans la méthode Event-B (1.5 h)
- Le raffinement d’un modèle Event-B (1.5 h)
- Introduction au Model-Checking (1.5 h)
- Validation d’une spécification Event-B par Model-Checking (1.5 h)
TP :
- Etude de cas - s1 (3.0 h)
- Etude de cas - s2 (3.0 h)