Verify UML statecharts with SMV

descriptionPublicationkeyboard_double_arrow_right Article 01 Mar 2001 English Publisher:EDP SciencesJournal:Wuhan University Journal of Natural Sciences, volume 6, pages 183-190 (issn: 1007-1202, eissn: 1993-4998,

Copyright policy )

Authors: Chen Hai-yan; Dong Wei; Wang Ji; Chen Huo-wang;

doi: 10.1007/bf03160241

Verify UML statecharts with SMV

- Summary
- Metrics

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.

Related Organizations

National University of Defense Technology
China (People's Republic of)
Wuhan University
China (People's Republic of)

Impact byBIP!

	selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	2
	popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.	Average
	influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	Average
	impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.	Average