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.

Macros used to configure our cases are:`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

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:

[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