by Sebastian Stock, Fabian Vu, David Geleßus, Michael Leuschel, Atif Mashkoor, Alexander Egyed
Abstract:
While refinement can help structure the modeling and proving process, it also forces the modeler to introduce features in a particular order. This means that features deeper in the refinement chain cannot be validated in isolation, making some reasoning unnecessarily intricate. In this paper, we present the AVoiR (Abstraction-Validation Obligation-Refinement) framework to ease validation of such complex refinement chains. The triptych AVoiR framework operates as follows: 1) We first simplify a complex model by abstracting away the noise, i.e., removing the information unrelated to properties under analysis. 2) Using the Validation Obligations (VOs) technique, we formalize the validation tasks of the desired property. 3) Finally, we trickle down the validation results by establishing the noiseless model as a parent of the initially investigated model through the standard refinement relationship. Furthermore, by using the technique of VO refinement, we establish the VOs of the abstract model on the initial model. We use a case study from the aviation domain to show the proposed framework's effectiveness.
Reference:
Validation by Abstraction and Refinement (Sebastian Stock, Fabian Vu, David Geleßus, Michael Leuschel, Atif Mashkoor, Alexander Egyed), In Rigorous State-Based Methods (Uwe Glässer, Jose Creissac Campos, Dominique Méry, Philippe Palanque, eds.), Springer Nature Switzerland, 2023.
Bibtex Entry:
@Conference{Stock2023a,
author = {Sebastian Stock and Fabian Vu and David Gele{\ss}us and Michael Leuschel and Atif Mashkoor and Alexander Egyed},
booktitle = {Rigorous State-Based Methods},
title = {Validation by Abstraction and Refinement},
year = {2023},
address = {Cham},
editor = {Gl{\"a}sser, Uwe and Creissac Campos, Jose and M{\'e}ry, Dominique and Palanque, Philippe},
pages = {160--178},
publisher = {Springer Nature Switzerland},
abstract = {While refinement can help structure the modeling and proving process, it also forces the modeler to introduce features in a particular order. This means that features deeper in the refinement chain cannot be validated in isolation, making some reasoning unnecessarily intricate. In this paper, we present the AVoiR (Abstraction-Validation Obligation-Refinement) framework to ease validation of such complex refinement chains. The triptych AVoiR framework operates as follows: 1) We first simplify a complex model by abstracting away the noise, i.e., removing the information unrelated to properties under analysis. 2) Using the Validation Obligations (VOs) technique, we formalize the validation tasks of the desired property. 3) Finally, we trickle down the validation results by establishing the noiseless model as a parent of the initially investigated model through the standard refinement relationship. Furthermore, by using the technique of VO refinement, we establish the VOs of the abstract model on the initial model. We use a case study from the aviation domain to show the proposed framework's effectiveness.},
doi = {10.1007/978-3-031-33163-3_12},
isbn = {978-3-031-33163-3},
keywords = {LIT Secure and Correct Systems Lab, FWF I4744},
url = {https://link.springer.com/chapter/10.1007/978-3-031-33163-3_12},
}