Landing Gear System
New Case Study
Frederic Boniol and Virgine Wiels have worked out a case study for the ABZ 2014 conference as “a benchmark for techniques and tools dedicated to the verification of behavioral properties of systems”. The case study is titled “Landing gear system” and presents the requirements for the digital part of a landing gear system for aircraft.
You will find information regarding the mentioned case study in the following document:
Full formal specification
We have worked out a full formal specification for these requirements based on abstract state machines (ASMs), where we strove for traceability and general understandability. We have proved several safety properties and disproved one property. Thereby we have noted several inconsistencies, ambiguities and gaps in the requirements document.
4th International ABZ Conference
A summary of design rationales and our experiences with the case study will be published in the proceedings of the ABZ 2014 conference in Toulouse (France), wich will be held from June 2nd - June 6th 2014. The full ASM model, the proofs, and a summary of the deficiencies which we identified in the requirements document are given in the technical report.