The landing gear system specification by Boniol et al. is a proposed benchmark for comparing and evaluating different formal model checking approaches. The Landing gear system is the safety critical part of an aircraft and have to maneuver the gears
and associated doors.
The system consists of a mechanical part including devices of three landing sets (front, left, right) as well as a set of sensors for monitoring this devices, a digital part including the control software and a pilot interface consisting of an up/down handle and a set of lights to illustrate the current health state of the system.
In the normal event sequence, the pilot manipulates the handle (up or down), the digital part sends orders to the electro-valves in order to perform the desired motion of the doors/gears and informs the pilot via lights about the status of the command execution.
The expected behavior of the landing gear system has to satisfy several temporal constraints which are part of the proposed system specification.
Modeling with SAML:
The technical and behavioral similarity of three landing sets allows for the usage of the template design pattern in SAML. To model the failure performance of the landing gear system, failure components are used. In our model, for all failure components the occurrences are set to nondet (non-deterministic) and recovering to never.
Our model consists of the following components (state machines): pilot interface, analogical switch, electro-valves, three landing sets containing hydraulic cylinders for moving doors
and gears, and the computing module.
For this case study we model specific automata as boolean formulas. If at each time step we need to know the intern (previous) state of the automata then we cannot model this component with formulas. We showed that the state machines for the door cylinders can be avoided and
consequently the system state space is smaller and the landing gear system model is verifiable in shorter time.
In this case study, we were able to reduce the state space size by a factor of 2 11 . The size of the internal binary decision diagram (BDD) could be minimized by an average factor of 4.5. The verification time of the restructured model compared to the standard model was reduced by a factor of 43.