ACCUEIL

Consignes aux
auteurs et coordonnateurs
Nos règles d'éthique
Auteurs : soumettez
votre article en ligne
Autres revues >>

Technique et Science Informatiques

0752-4072
Revue des sciences et technologies de l'information
 

 ARTICLE VOL 34/5 - 2015  - pp.549-573  - doi:10.3166/tsi.34.549-573
TITRE
Premières leçons sur la spécification d’un train d’atterrissage en B Événementiel

TITLE
First lessons on the specification of a landing-system in Event-B

RÉSUMÉ
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 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, au moment de leur introduction, 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.


ABSTRACT
This article presents the preliminary lessons gained from developing in Event-B the case-study proposed for the ABZ2014 conference. The case is the modeling of the software control for the landing-gears system of a plane. The use of Event-B for this case-study raises interesting questions such as the nature of the invariants, the moment when they are introduced, as well as the expression and verification of the functional properties. The refinement chain is organized in observation levels structured following the hardware description. The system is seen as an automaton controled by external sensors. Describing such a system in Event-B is simple but validating it is much more difficult. This activity relies on JeB, a simulator for EventB in JavaScript. Emulating the sensors is a crucial issue.


AUTEUR(S)
Jean-Pierre JACQUOT

Reçu le 30 janvier 2015.    Accepté le 14 août 2015.

MOTS-CLÉS
méthodes formelles, validation, B Événementiel, JeB.

KEYWORDS
formal methods, validation, Event-B, JeB.

LANGUE DE L'ARTICLE
Français

 PRIX
• Abonné (hors accès direct) : 12.5 €
• Non abonné : 25.0 €
|
|
--> Tous les articles sont dans un format PDF protégé par tatouage 
   
ACCÉDER A L'ARTICLE COMPLET  (4,10 Mo)



Mot de passe oublié ?

ABONNEZ-VOUS !

CONTACTS
Comité de
rédaction
Conditions
générales de vente

 English version >> 
Lavoisier