A Model Checker for Statecharts

Computer-Aided Software Engineering (CASE) tools encourage users to codify the specification for the design of a system early in the development process. They often use graphical formalisms, simulation and prototyping to help express ideas concisely and unambiguously. Some tools provide little more than syntax checking of the specification but others can test the model for reachability of conditions, nondeterminism or deadlock.

Formal methods include powerful tools like automatic model checking to exhaustively check a model against certain requirements. Integrating formal techniques into the system development process is an effective method of providing more thorough analysis of specifications than conventional approaches employed by Computer-Aided Software Engineering (CASE) tools. In order to create this link, the formalism used by the CASE tool must have a precise formal semantics that can be understood by the verification tool.

The CASE tool STATEMATE makes use of an extended state transition notation called statecharts. We have formalized an operational semantics for statecharts by embedding them in the logical framework of an interactive proof-assistant system called HOL. A software interface is provided to extract a statechart directly from the STATEMATE database.

Using HOL in combination with Voss, a binary decision diagram-based verification tool, we have developed a model checker for statecharts which tests whether an operational specification, given by a statechart, satisfies a descriptive specification of the system requirements. The model checking procedure is a simple higher-order logic function which executes the semantics of statecharts.

In this technical report, we describe the formal semantics of statecharts and the model checking algorithm. Various examples, including an intersection with a traffic light and an arbiter, are presented to illustrate the method.