Landing Gear System

The model

The model is available in this archive. Due to a large number of configurations, a preprocessor (GPP) was used to produce individual cases. The archive contains a Makefile that can be used to produce all cases.

• FAILURES accepts TRUE / FALSE
• DUPLICATE_DIGITAL_COMPONENT which accepts TRUE / FALSE (not used in provided cases)
• GEARS_SETS which V1 (one gear set) and V3 (three gear sets)
• CYLINDER_CONSTRAINTS which accepts MIN_MAX (times with 20% variation) and MAX_MAX (exact times without variation)
• BOUND_HANDLE which accepts TRUE / FALSE and sets the pilot behavior (bounded / unbounded)
• MAX_HANDLE_OPS which accepts an integer and defines the number of handle moves of a bounded pilot
• more macros are available in LandingSystem.fcr...

The model can also be retrieved as individual files:

• LandingSystem.fcr : the model (cannot be used by fiacre without preprocessing)
• LandingSystemDiscrete.fcr : discrete version of the model (cannot be used by fiacre without preprocessing)
• minmax.def : timing constraints used in the model (inlined by preprocessor)
• maxmax.def : timing constraints used in the model (inlined by preprocessor)
• Makefile : the Makefile

Generated cases

If you do not want to install GPP, an archive containing generated cases is available here

But you can also retrieve each case, where:

• F means with failures
• N means without failures (normal mode)
• V1 means one door/gear set
• V3 means three door/gear sets
• H1[X] is a bounded scenario where the pilot moves the handle X times
• H2 is an un bounded scenario, ie. the pilot can move handle infinitely

Cases:

• case_F_V1_H1[02].fcr
• case_F_V1_H1[03].fcr
• case_F_V1_H1[04].fcr
• case_F_V1_H1[05].fcr
• case_F_V3_H1[02].fcr
• case_F_V3_H1[03].fcr
• case_F_V3_H1[04].fcr
• case_F_V3_H1[05].fcr
• case_N_V1_H1[08].fcr
• case_N_V1_H1[09].fcr
• case_N_V1_H1[10].fcr
• case_N_V1_H1[11].fcr
• case_N_V1_H1[12].fcr
• case_N_V1_H2.fcr
• case_N_V3_H1[08].fcr
• case_N_V3_H1[09].fcr
• case_N_V3_H1[10].fcr
• case_N_V3_H1[11].fcr
• case_N_V3_H1[12].fcr
• case_N_V3_H2.fcr

We also provide cases for on the fly model checking of requirement R1.1. Here the pilot will some times wait X seconds before performing another move. We can detect the state of the pilot and check if gears are retracted and doors are closed. This test can be performed on the fly using command:

sift case_N_V3_H2_8500.tts -E -f "Pilot_1_shandle__up__elapsed => (LandingSystem_w1 /\ LandingSystem_w3)"

Cases:

• case_N_V3_H2_15000.fcr
• case_N_V3_H2_9000.fcr
• case_N_V3_H2_8400.fcr
• case_N_V3_H2_8500.fcr

References

[BDF2014] Model-Checking Real-Time Properties of an Aircraft Landing Gear System Using Fiacre, B. Berthomieu, S. Dal Zilio and L. Fronc, 4th International ABZ 2014 Conference.

[WB2014] Landing Gear System, Case study for the ABZ 2014 conference, V. Wiels and F. Boniol