Abstract State Machines (ASMs) are widely used in the formalization and verification of the semantics of software or hardware. However, tools for assisting this process for evolving specifications are still lacking. With evolving we denote adding extensions without refactoring. We want to create a tool assisting in the verification of evolving specifications. Our approach is to translate ASM specifications into the language of an existing proof checker, construct the proofs as far as possible automatically, and check the proofs with the proof checker. Further, we want proofs of evolvable specifications also to be evolvable. This paper gives a brief overview of the approach and discusses the first step of this work, namely the translation of ASM specifications into the language of an existing proof checker, with consideration of automation possibilities.
If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.
% BibTex
@inproceedings{Sabinus24,
author = {Edward Sabinus},
editor = {Silvia Bonfanti and
Angelo Gargantini and
Michael Leuschel and
Elvinia Riccobene and
Patrizia Scandurra},
title = {Proof Construction and Checking on Evolving Abstract State Machines},
booktitle = {Rigorous State-Based Methods - 10th International Conference, {ABZ}
2024, Bergamo, Italy, June 25-28, 2024, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {14759},
pages = {392--396},
publisher = {Springer},
year = {2024},
url = {https://doi.org/10.1007/978-3-031-63790-2\_30},
doi = {10.1007/978-3-031-63790-2\_30},
timestamp = {Thu, 04 Jul 2024 22:05:23 +0200},
biburl = {https://dblp.org/rec/conf/zum/Sabinus24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}