基于有色Petri网的SysML序列图的分析与验证

Analysis and verification of SysML sequence diagrams based on colored Petri net

针对SysML序列图本身缺乏分析和验证手段的问题,提出了一种序列图到有色Petri网的转换方法:定义了将序列图的常用操作转换为等价有色Petri网的转换规则,重点是把序列图的常用结构如可选结构、条件结构、并行结构以及循环结构等映射为有色Petri网。这当中既包含结构元素,如库所、变迁、输入/输出弧,又包含逻辑元素,如全局声明中的颜色集和变量、颜色集与库所、弧表达式以及初始标志。应用这些规则可以将序列图转换为有色Petri网模型,进而对其进行仿真分析,并可通过有色Petri网工具验证模型的无死锁性、可达性、有界性和活性。最后通过数字证书更新的实例分析了映射前后两种模型的语义,验证了映射的正确性。

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