EventB
Ref: 3IF2250
Description
Ce cours permettra aux étudiants de découvrir les concepts de base de la méthode B à travers les activités de modélisations et de la preuve en utilisant l'Atelier B, l'IDE principal de la méthode 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 B, et de générer automatiquement un code C vérifié et conforme à la spécification initiale. L'animation de modèles B en utilisant l'outils ProB est également abordée.
A 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.
Période(s) du cours
SM11
Prérequis
Cursus commun en informatique
Syllabus
- C1-C2 (CM-TD) : Le langage B
- La théorie des ensembles
- La logique du 1e ordre et la Logique de Hoare.
- Les substitutions généralisées et le calcul de la plus faible pré-condition de Dijkstra
- C3-C4 (CM-TD) : Le modèle B
- La modélisation d'un système en utilisant la méthode B classique
- Le raffinement d'un système en B
- C5-C6 (CM-TD) : La preuve en B
- Les obligations de preuve d'un modèle B
- La preuve interactive avec l'atelier B
- C7-C8 (CM-TD) : Le modèle checking en B
- C9-C10 (CM-TD) : L'implémentation d'un modèle B
- Génération de code par raffinement
- C11-C14 (TP) : TP sur machine
Composition du cours
- Cours magistraux pour présenter les concepts
- TD/TP pour mettre en œuvre les concepts
Ressources
Les pratiques utilisés dans ce cours combinent cours magistraux et TD favorisant une pratique concrète sur les outils existants autour de la méthode B.
Résultats de l'apprentissage couverts par le cours
À l'issu de ce cours, les étudiants seront capables de :
- modéliser avec la méthode B.
- manipuler les notions de Machine abstraite et de raffinement.
- établir la preuve de consistence d'un modèle B et de son raffinement (avec le prouveur de l'Atelier B).
- animer un modèle B (avec le model-checker Pro-B).
- générer un code vérifié à partir d'un modèle B
- développer des logiciels critiques
Support de cours, bibliographie
- Jean-Raymond Abrial, The B-Book, Cambridge University Press, 1996
- https://www.clearsy.com/wp-content/uploads/sites/3/ressources/manrefb1.8.6.uk.pdf | B LANGUAGE REFERENCE MANUAL