Verify UML statecharts with SMV
Chen Hai-yan, Wei Yu Dong, Ji Wang, Huowang Chen · Wuhan University Journal of Natural Sciences · 2001
Formal verification has been widely needed in the development of safety critical systems. In order to introduce the design verification activity in UML developing process, we have developed a verifier of UML Statecharts by using the model checker SMV. The approach is to transform a system model in UML Statecharts to one in SMV input language via an intermediate language and then to verify the system properties specified in CTL by invoking SMV. The current experiences, including the formal verification of a simplified directory based cache coherence protocol in UML Statecharts, show that automatic verification can be integrated as a new step of the software process nicely.