Model checking statecharts based on conditional term rewriting systems

Formal verification of statecharts with the use of current model checking techniques is the main concern of this paper. To model check it, however, its description has to be translated into the input language of the model checker. This paper describes how statecharts can be translated into SMV to allow for branching time model checking of statecharts. To reflect statecharts as close as in SMV, we encoded statecharts as conditional rewrite rules which serves as a bridge between them. We defined its operational semantics which guides the correct translation. This paper also described the translation techniques of advanced features of statecharts such as history states and conflict resolutions.