Validation of the ABZ landing gear system using ProB

Lukas Ladenberger, Dominik Hansen, Harald Wiegard, Jens Bendisposto, Michael Leuschel
Printed Source Abstract Cite
Type
Journal article
Publication
International Journal on Software Tools for Technology Transfer (STTT)

Abstract

In this article, we present our formalization 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 the visualization features provided by ProB and BMotion Studio. In addition, we discuss the positive and negative aspects of the Event-B language and tools which we encountered while working on the ABZ case study.

Reference

% BibTex
@Article{Ladenberger2017,
author="Ladenberger, Lukas
and Hansen, Dominik
and Wiegard, Harald
and Bendisposto, Jens
and Leuschel, Michael",
title="Validation of the ABZ landing gear system using ProB",
journal="International Journal on Software Tools for Technology Transfer",
year="2017",
month="Apr",
day="01",
volume="19",
number="2",
pages="187--203",
abstract="In this article, we present our formalization 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 the visualization features provided by ProB and BMotion Studio. In addition, we discuss the positive and negative aspects of the Event-B language and tools which we encountered while working on the ABZ case study.",
issn="1433-2787",
doi="10.1007/s10009-015-0395-9",
url="https://doi.org/10.1007/s10009-015-0395-9"
}

Model Archive : Not available Presentation : Not available Used formal method : ProB Resources and tools : ProB Required OS : Linux Website : Not available Remarks and recommendation : No

ABZ'14

Related