Skip to Main content Skip to Navigation
Conference papers

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 - FM - Department of Formal Methods
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.
Document type :
Conference papers
Complete list of metadata

Cited literature [13 references]  Display  Hide  Download

https://hal.inria.fr/hal-00982982
Contributor : Jean-Pierre Jacquot <>
Submitted on : Thursday, April 24, 2014 - 3:53:07 PM
Last modification on : Tuesday, December 18, 2018 - 4:38:25 PM
Long-term archiving on: : Thursday, July 24, 2014 - 11:31:00 AM

File

version-HAL.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00982982, version 1

Collections

Citation

Jean-Pierre Jacquot. Premières leçons sur la spécification d'un train d'atterrissage en B événementiel. AFADL 2014, CNAM - Cédrics, Jun 2014, Paris, France. ⟨hal-00982982⟩

Share

Metrics

Record views

602

Files downloads

739