ABZ 2014: The Landing Gear Case Study - Case Study Track at ABZ 2014
|Titel||ABZ 2014: The Landing Gear Case Study - Case Study Track at ABZ 2014|
|Serie||Communications in Computer and Information Science|
Case studies have played an essential role in the history of formal methods. They allowed to illustrate the application of formal techniques for modelling and verification, to compare different methods in terms of expressivity, performance and easiness of use. They have also permitted to enact the progress made by these methods. As formal methods have made a lot of progress over the years, ABZ 2014 proposed a complex case study as representative of industrial needs.
The proposed case study, a landing gear system for an aircraft, is composed of three parts: the pilot interface, the mechanical and hydraulic parts, and the digital part. The case study is thus not restricted to software, but involves complex system modelling (behavior of gears, doors, cylinders, electrovalves). The software part is in charge of controlling gears and doors, but also of monitoring the system and informing the pilot in case of an anomaly. Requirements to be verified on the system include normal mode and failure mode requirements. In both categories, requirements combine functional properties and timing constraints. This case study is indeed complex, to model and to verify. Furthermore, it was not a priori a state-based oriented case study and a question was indeed to see how the ABZ formal methods could accommodate this kind of system.
We were very happy that the case study attracted a lot of interest. The 11 selected papers use different formal techniques: B, ASM, Fiacre. They also propose different kinds of verification: proof, model checking, test generation, run-time monitoring, and simulation. The papers did not necessarily model all aspects of the case study, but the proposed modelling and analyses were very interesting.
In addition to the submissions, a lot of interest has been expressed for this case study. We had a lively and stimulating track during the 4th edition of the ABZ'2014 conference in Toulouse, with fruitful discussions around obtained results.