Here we present three formal developments in our paper “Wen Su, Jean-Raymond Abrial. Aircraft Landing Gear System: Approaches with Event-B to the Modeling of an Industrial System”.

Introduction

The entire model of those examples can be obtained as source model of the Rodin Platform.

For those who are interesting to check the models with the Rodin Platform, here are some information: if you have not yet downloaded the Rodin Platform, please download the newest version from the website: http://www.event-b.org. If you have already got the Platform, please make sure that you have installed the plug-in of Atelier B and SMT solver.

Please use the default tactic profile of SMT solver called “Default Atuo Tactic with SMT (do not edit)”. This is the tactic profile we used for all the proofs. When SMT solver has already been installed, in order to change to the tactic profile mentioned, please go to: Preferences –> Event-B –> Sequent Prover –> Auto/Post Tactic, in the the tag “Auto/Post Tactic”, enable both the auto-tactic and the post-tactic for proving, and set them both to “Default Atuo Tactic with SMT (do not edit)”.

We also recommend the plug-in AnimB or ProB for animation. In order to use AnimB, please check your editor, since only Event-B Context Editor is supported by AnimB. Moreover, ProB is also used as a model checker to find counterexamples.

Contact

If you have any question, please don’t hesitate to contact us: wsu@shu.edu.cn

Rodin Development

In the paper “Aircraft Landing Gear System: Approaches with Event-B to the Modeling of an Industrial System”, we follow the naming convention that all the physical variables are in capital letters. However, in the Rodin development below, they are still kept in lower letters. Here we give the mapping list:

In the First Approach:
handle –> HNDL
door_closed –> DOOR_CLOSED
door_open –> DOOR_OPEN
door_closing –> DOOR_CLOSING
door_opening –> DOOR_OPENING
analogical_switch –> ANALOGICAL_SWITCH
ana_closing –> ANA_CLOSING
green_light –> GREEN_LIGHT
orange_light –> ORANGE_LIGHT
red_light –> RED_LIGHT

In the Second Approach:
prs –> PRS
dpr –> DPR
doors_opn –> DOORS_OPN
doors_cls –> DOORS_CLS
gears_rtr –> GEARS_RTR
gears_ext –> GEARS_EXT

Download

  • First Approach
Landing_Dev_1.zip Landing_Dev_1.pdf
  • Second Approach
Landing_Dev_2.zip Landing_Dev_2.pdf
  • Third Approach
Landing_Dev_3.zip Landing_Dev_3.pdf
  • Reachability Model
Land_Variant_2.zip Landing_Variant_2.pdf
  • All Three Approaches and Reachability Model
ALL.zip ALL.pdf