An Approach Converting XMI to SMV

다국어 초록 (Multilingual Abstract)

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.

목차 (Table of Contents)

• Abstract
• 1. Introduction
• 2. Related Conceptions
• 2.1. Model Checking
• 2.2. NuSMV [4]
• 2.3. Finite State Machine
• 2.4. UML State Diagram and XMI
• 3. From XMI to SMV Process
• 3.1. The NuSMV Input Language
• 3.2. Mapping Rule
• 3.3. XMI2SMV Architecture
• 3.4. Realise XMI2SMV in Python
• 4. A Case Study
• 4.1. Modeling based on FSM
• 4.2. Generating Code
• 4.3. Run Code
• 5. Conclusion
• References