›› 2012, Vol. 25 ›› Issue (2): 100-.

• Articles • Previous Articles     Next Articles

Consistency Check Between UML State Chart and Sequence Chart Based on Model Checking

 DU Jie, JIANG Guo-Hua   

  1. (School of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 210016,China)
  • Online:2012-02-15 Published:2012-02-29


UML can be used to accomplish the system modeling from different views.There may be some redundancy in different views,so that the views may be inconsistent.This paper proposes modeling methods based on the formalization method and the UML.It focuses mainly on using the model checking to check the consistency between the UML statechart and the sequence chart.The method to deal with the composite sequence chart is proposed and the hierarchy structure of the statechart is translated into the finite automata machine.Then the NuSMV is used to verify them.Experimental results show the effectiveness of the converting methods.

Key words: UML;model checking;NuSMV

CLC Number: 

  • TP311.55