Statecharts and Message Sequence Charts (MSCs) have been widely used for specifying dynamic behavior of a system. In recent years, both statecharts and MSCs are used simultaneously to specify different aspects of the same system. In this paper we discuss how consistency between Statecharts and MSCs can be checked formally.
We define the semantics of Statecharts and MSCs in terms of Buchi-automata and consistency between Statecharts and MSCs in terms of the language containment relationship between the resulting Buchi-automata. We verify the consistency using the model checking, especially the model checker SMV for efficiency, and define rules for translating Statecharts and MSCs into the input of SMV. We develop an tool which supports the automatic verification of consistency checking problems using the model checker SMV.
