Skip to Main content Skip to Navigation
Journal articles

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
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.
Document type :
Journal articles
Complete list of metadata
Contributor : Jean-Pierre Jacquot <>
Submitted on : Tuesday, January 26, 2016 - 11:16:10 AM
Last modification on : Monday, November 30, 2020 - 4:44:08 PM




Jean-Pierre Jacquot. Premières leçons sur la spécification d’un train d’atterrissage en B Événementiel. Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, Lavoisier, 2016, 34 (5), pp.549-573. ⟨10.3166/TSI.34.547-571⟩. ⟨hal-01262077⟩



Record views