Verify UML statecharts with SMV |
| |
| Authors: | Chen Hai-yan Dong Wei Wang Ji Chen Huo-wang |
| |
| Institution: | 1. Department of Computer Science, National University of Defense Technology, 410073, Changsha, China
2. State Key Laboratory for Software Engineering, Wuhan University, 430072, Wuhan, China
|
| |
| Abstract: | 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. |
| |
| Keywords: | |
| 本文献已被 SpringerLink 等数据库收录！ |
|
