We present an ASM model for the case study given as a challenge for the ABZ'14 conference, which specifies the digital part of a landing gear system for aircraft. We strove to make the formal model well understandable for humans. We note inconsistencies, ambiguities and gaps in the case study and summarise our experiences during modelling and the proof of safety properties.
% BibTex
@inproceedings{ABZ2014-Landing-Gear-System-Case-Study,
author = {Boniol, Fr\'ed\'eric and Wiels, Virginie},
title = {{T}he {L}anding {G}ear {S}ystem {C}ase {S}tudy},
booktitle = {ABZ Case Study},
year = {2014},
publisher = {Springer},
series = {Communications in Computer Information Science},
volume = {433},
}
@MISC{BoniolWiels2013,
title = {Landing gear system},
author = {Frederic Boniol and Virginie Wiels},
year = {2013},
howpublished = {Challenge for the {ABZ}'14 conference, \url{http://www.irit.fr/ABZ2014/landing_system.pdf}, accessed 2013-12-19}
}
@BOOK{BoergerStaerk2003,
title = {Abstract State Machines - A Method for High-Level System Design and
Analysis},
publisher = {Springer Verlag},
year = {2003},
author = {Egon B\"orger and Robert St\"ark}
}
@MISC{Kossak2014,
title = {Landing Gear System: An {ASM}-based Solution for the {ABZ'14} Case Study. {Technical Report SCCH-TR-1401} with the complete model and proofs},
author = {Felix Kossak},
year = {2014},
howpublished = {\url{http://www.scch.at/en/rse-news/landing_gear}}
}
@INPROCEEDINGS{KossakEtal2014,
author = {Felix Kossak and Atif Mashkoor and Verena Geist and Christa Illibauer},
title = {Improving the Understandability of Formal Specifications: An Experience Report},
booktitle = {Proc. of the 20th Conf. on Requirements Engineering: Foundation for Software Quality (REFSQ'14; to appear)},
year = {2014}
}