Premières leçons sur la spécification d'un train d'atterrissage en B événementiel
Résumé
Ce papier présente les leçons préliminaires obtenues en traitant en B Événementiel l'étude de cas proposée par la conférence ABZ 2014. Le problème consiste à modéliser le logiciel de contrôle du train d'atterrissage d'un avion. L'utilisation de B Évémentiel sur cette étude pose des questions intéressantes quant à la nature des invariants, quant au moment de leur introduction, ainsi que quant à l'expression et la vérification des propriétés fonctionnelles. Le raffine- ment est organisé en niveaux d'observation structurés par la description du maté- riel. Le système est vu comme un automate assez simple piloté par des capteurs externes. La description d'un tel système en B Événementiel est simple mais sa validation est beaucoup plus difficile. Cette étape utilise JeB, un simulateur de B Événementiel en JavaScript. L'émulation des capteurs est un point crucial.
Domaines
Génie logiciel [cs.SE]
Origine : Fichiers produits par l'(les) auteur(s)
Loading...