Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, EpiSciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
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 Connect in order to contact the contributor
Submitted on : Thursday, April 24, 2014 - 3:53:07 PM
Last modification on : Saturday, October 16, 2021 - 11:26:08 AM
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

214

Files downloads

400