基于随机Petri网的SysML状态机图的验证

摘要

For solving the problem of SysML in lacking analysis and verification means by itself,this paper presents a method of converting the SysML state machine diagram to generalised stochastic Petri net,in main there are eight transformation rules defined for converting the SysML state machine diagram to corresponding executable model of Petri net.Using these transformation rules,the SysML state machine diagram can be transformed to Petri net,and then to further analyse and verify it.Besides of this,the rules can also be used to detect concurrency-related code of conduct nature,such as deadlocks,boundness,etc.At the same time,the method can handle state transition with time delay and information probability.Finally,an example of digital certificates systems is used to demonstrate the feasibility of the method.%针对SysML状态机图本身缺乏分析和验证手段的问题,提出一种SysML状态机图向广义随机Petri网的转换方法.主要定义将SysML状态机图转换为相应Petri网可执行模型的八种转换规则,应用这些规则可以将状态机图转换为Petri网模型,进而对其进行分析、验证,并可检测SysML的行为规范与并发相关的性质,如死锁、有界性等,同时,该方法可处理带有时间延迟和概率信息的状态转换.最后通过数字证书系统的一个实例说明该方法的可行性.