Third Asia-Pacific Software Engineering Conference (APSEC'96)
Formalization and Verification of Safety Properties of Statechart Specifications
Seoul, SOUTH KOREA
December 04-December 07
ISBN: 0-8186-7638-8
There have been many analysis methods proposed for the verification of safety properties of real-time systems. Most of these methods, however, are not powerful enough for complex and safety-critical real-time systems due mainly to the lack of language primitives for specifying complex requirements (e.g., ESM) or heuristic verification procedures that do not provide verification results with certainty (e.g., Statechart and Modechart). In this paper, a new approach for the verification of safety properties of real-time systems is introduced. This approach adopts Statechart to specify real-time systems behaviors. We redefined the step semantics of Statechart to address problems of the synchrony hypothesis inherent to the original step semantics. A operational semantics of Statechart is defined based on the step semantics and a verification method for safety properties was developed based on the operational semantics of Statechart. This method verifies safety properties against a reachability graph derived from a Statechart diagram. We did not sacrifice the practicality or expressive power of Statechart for the simplification of analysis. Useful event and action primitives including the time-out event tm( ) and scheduled-action sc!( ) are included in the analysis. A Train-Gate System is used as an example to illustrate the concepts in this paper.
Index Terms:
real-time system, safety property, Statecharts, reachability graph, temporal logic, specification technique.
Citation:
Kyo C. Kang, Kwang-Il Ko, "Formalization and Verification of Safety Properties of Statechart Specifications," apsec, pp.16, Third Asia-Pacific Software Engineering Conference (APSEC'96), 1996