Title :
Implementing statecharts in PROMELA/SPIN
Author :
Mikk, Erich ; Lakhnech, Yassine ; Siegel, Michael ; Holzmann, Gerard J.
Author_Institution :
Inst. fur Inf. und Praktische Math., Kiel Univ., Germany
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 a 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
Keywords :
computer aided software engineering; program interpreters; program verification; CASE-tool; PROMELA/SPIN; SPIN verification system; STATEMATE; extended hierarchical automata; iLogix; input language; linear temporal logic model checking; parallel code; sequential code; statecharts; translator; Aerospace electronics; Art; Automata; Automatic control; Communication system control; Computer aided software engineering; Documentation; Ear; Licenses; Logic;
Conference_Titel :
Industrial Strength Formal Specification Techniques, 1998. Proceedings. 2nd IEEE Workshop on
Conference_Location :
Boca Raton, FL
Print_ISBN :
0-7695-0081-1
DOI :
10.1109/WIFT.1998.766303
