Premières leçons sur la spécification d’un train d’atterrissage en B Événementiel

Jean-Pierre Jacquot 1
1 DEDALE - Development of specifications
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Cet article 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 logi- ciel 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, au moment de leur introduc- tion, ainsi qu’à l’expression et la vérification des propriétés fonctionnelles. Le raffinement est organisé en niveaux d’observation structurés par la description du matériel. Le système est vu comme un automate 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.
Type de document :
Article dans une revue
Technique et Science Informatiques, Hermès-Lavoisier, 2016, pp.25. 〈10.3166/TSI.34.547-571〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01262077
Contributeur : Jean-Pierre Jacquot <>
Soumis le : mardi 26 janvier 2016 - 11:16:10
Dernière modification le : jeudi 11 janvier 2018 - 06:20:08

Identifiants

Collections

Citation

Jean-Pierre Jacquot. Premières leçons sur la spécification d’un train d’atterrissage en B Événementiel . Technique et Science Informatiques, Hermès-Lavoisier, 2016, pp.25. 〈10.3166/TSI.34.547-571〉. 〈hal-01262077〉

Partager

Métriques

Consultations de la notice

119