Analysis and verification of SysML sequence diagrams based on colored Petri net
基于有色Petri网的SysML序列图的分析与验证

Aiming at the problems of SysML sequence diagrams lack of analysis and verification methods,this paper presented a method for conversing sequence diagrams to the colored Petri net,defining the equivalent conversion rules for converting sequence diagrams of the common operations into a colored Petri net,mainly focusing on mapping sequence diagram’s common structure such as optional structures,alternate structures,parallel structure and loop structure into colored Petri nets.They not only contained structure elements,such as place,transition,input and output arcs,but also contained the logic elements,such as the global declaration of the color sets and variables,color sets and places,and the initial marking,arc expression.Using these transformation rules,the method could transform sequence diagrams into colored Petri nets,and made its simulation and analysis.Besides of this,it could verify the characters of the model,such as absence-deadlocks,boundness,liveness,etc.Finally,the examples of digital certificates updated analysed the semantic of the model before and after mapping,verified the correctness of the mapping.