Earticle

초록

영어

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.

목차

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

키워드

저자

• Rongshang Chen [ College of Computer and Information Engineering, Xiamen university of Technology, Xiamen, China ]
• Jinyu Kai [ School of Computer Engineering and Science, AnYang Normal University, AnYang, China ]
• MingXu [ College of Computer and Information Engineering, Xiamen university of Technology, Xiamen, China ]
• LeiXiao [ Xiamen Institute of Software Technology ]

참고문헌

발행기관

간행물

표지보기 관심저널 등록

• 간행물명

  International Journal of Security and Its Applications

• 간기

  격월간

• pISSN

  1738-9976

• 수록기간

  2008~2016

• 등재여부

  SCOPUS

• 십진분류

  KDC 505 DDC 605