by Stock, Sebastian, Vu, Fabian, Geleßus, David, Leuschel, Michael, Mashkoor, Atif and Egyed, Alexander
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:
Stock, Sebastian, Vu, Fabian, Geleßus, David, Leuschel, Michael, Mashkoor, Atif and Egyed, Alexander: Validation by Abstraction and Refinement, in Rigorous State-Based Methods (Glässer, Uwe, Creissac Campos, Jose, Méry, Dominique, Palanque, Philippe, eds.), Springer Nature Switzerland, 2023.
Bibtex Entry:
@Conference{Stock2023a,
author = {Stock, Sebastian and Vu, Fabian and Gele{\ss}us, David and Leuschel, Michael and Mashkoor, Atif and Egyed, Alexander},
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},
}