Abstract In this paper we present our formalisation of the ABZ landing gear case study in Event-B. The development was carried out using the Rodin platform and mainly used superposition refinement to structure the specification. To validate the model we complemented proof with animation and model checking. For the latter, we used the ProB animator and model checker. Graphical representation of the model turned out to be crucial in the development and validation of the model; this was achieved using a new version of BMotion Studio integrated into ProB 2.0.
Validation of the ABZ Landing Gear System Using ProB
2014-01-01
14 pages
Article/Chapter (Book)
Electronic Resource
English
Validation of the ABZ Landing Gear System Using ProB
British Library Conference Proceedings | 2014
|