期刊名称：International Journal of Security and Its Applications
印刷版ISSN：1738-9976
出版年度：2015
卷号：9
期号：12
页码：323-330
DOI：10.14257/ijsia.2015.9.12.30
出版社：SERSC
摘要：The technique of model checking is playing a more and more important role in formal verification and automated software testing. When using the model checker tool NuSMV, people have to program the code for the model they built firstly. During the course of programming with the input language of NuSMV, for non-expert users, some manual mistakes may be brought in such as making syntax errors or omitting some transfer conditions etc. This paper introduces a tool XMI2SMV which is an automatic generator to be used to generate NuSMV programming codes for XMI files. This tool aims to bridge between a UML tool and the model checker tool NuSMV. We just need build our behavioral system model using a UML tool and export its corresponding XMI file, and this tool can help us to generate NuSMV code automatically, avoiding manual errors.
关键词：Model Checking; NuSMV; FSM; UML State Diagram; XMI; SMV codes
