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.
Type de document :
Communication dans un congrès
C. Dubois; R. Laleau. AFADL 2014, Jun 2014, Paris, France. 2014
Liste complète des métadonnées

Littérature citée [13 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00982982
Contributeur : Jean-Pierre Jacquot <>
Soumis le : jeudi 24 avril 2014 - 15:53:07
Dernière modification le : mardi 24 avril 2018 - 13:34:10
Document(s) archivé(s) le : jeudi 24 juillet 2014 - 11:31:00

Fichier

version-HAL.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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. C. Dubois; R. Laleau. AFADL 2014, Jun 2014, Paris, France. 2014. 〈hal-00982982〉

Partager

Métriques

Consultations de la notice

524

Téléchargements de fichiers

442