Model checking consistency of sequence diagram and state machine based on state reduction
Qian Chen · Jisuanji yingyong yanjiu · 2014
The proposed a new method for model checking the consistency of the semantics of sequence diagram and state machine in the process of design.The method formalized the description of the consistency of sequence and state machine to establish the theoretical basis of model checking.This paper presented some state reduction rules and a state reduction algorithm which proved not affect the consistency to decrease the redundancy of states and transitions.Moreover,it translated the UML model to PROMELA which was the specification language of the model checker SPIN which was used to verify the consistency.Experiments indicate that,consistency of sequence diagram and state machine diagram is effectively verified,states and transitions are decreased during the model checking process,and the codes generated are simpler and more effective.