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
|
Landing_Dev_1.zip | Landing_Dev_1.pdf |
|
Landing_Dev_2.zip | Landing_Dev_2.pdf |
|
Landing_Dev_3.zip | Landing_Dev_3.pdf |
|
Land_Variant_2.zip | Landing_Variant_2.pdf |
|
ALL.zip | ALL.pdf |