Statechart notations with ‘run to completion’ semantics, are popular with engineers for designing controllers that respond to events in the environment with a sequence of state transitions. However, they lack formal refinement and rigorous verification methods. , on the other hand, is based on refinement from an initial abstraction and is designed to make formal verification by automatic theorem provers feasible. We introduce a notion of refinement into a ‘run to completion’ statechart modelling notation, and leverage tool support for theorem proving. We describe the difficulties in translating ‘run to completion’ semantics into refinements and suggest a solution. We outline how safety and liveness properties could be verified.
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{MorrisSHHAB20,
author = {Karla Morris and
Colin F. Snook and
Thai Son Hoang and
Geoffrey C. Hulette and
Robert C. Armstrong and
Michael J. Butler},
editor = {Alexander Raschke and
Dominique M{\'{e}}ry and
Frank Houdek},
title = {Refinement and Verification of Responsive Control Systems},
booktitle = {Rigorous State-Based Methods - 7th International Conference, {ABZ}
2020, Ulm, Germany, May 27-29, 2020, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {12071},
pages = {272--277},
publisher = {Springer},
year = {2020},
url = {https://doi.org/10.1007/978-3-030-48077-6\_23},
doi = {10.1007/978-3-030-48077-6\_23},
timestamp = {Mon, 03 Jan 2022 22:35:01 +0100},
biburl = {https://dblp.org/rec/conf/asm/MorrisSHHAB20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}