Published Articles >> Table of Contents >> Abstract

Second IEEE Workshop on Industrial Strength Formal Specification Techniques   p. 90
Implementing Statecharts in PROMELA/SPIN
Erich Mikk, Christian-Albrechts Universität zu Kiel
Yassine Lakhnech, Christian-Albrechts Universität zu Kiel
Michael Siegel, Christian-Albrechts Universität zu Kiel
Gerard J. Holzmann, Bell Laboratories

Full Article Text:

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/WIFT.1998.766303
Send link to a friend

Abstract
We translate statecharts into PROMELA, the input language of the SPIN verification system, using extended hierarchical automata as an intermediate format We discuss two possible frameworks for this translation, leading to either sequential or parallel code. We show that in this context the sequential code can be verified more efficiently than the parallel code. We conclude with the discussion of an application of the resulting translator to a well-known case study, which demonstrates the feasibility of linear temporal logic model checking of statecharts.
Back to Top Additional Information
Citation:  Erich Mikk, Yassine Lakhnech, Michael Siegel, Gerard J. Holzmann, "Implementing Statecharts in PROMELA/SPIN," wift, p. 90,  Second IEEE Workshop on Industrial Strength Formal Specification Techniques,  1998