基于扩展Petri网的系统建模及形式化验证方法

Methodology of modeling and formal verification based on extended Petri net

嵌入式实时系统对时间约束性、安全性和可靠性具有非常高的要求,但是传统的建模和形式化验证方法难以满足对系统的实时性和安全性的模拟和验证需求。通过对有色Petri网的时间属性进行扩展,提出了实时有色Petri网模型,能够对系统的时间属性进行模拟和评估;参考实时有色Petri网模型到时间自动机的语义转换规则对模型进行转换,可以利用时间计算树逻辑对系统的实时性、安全性和可靠性进行形式化验证。以列车通信网络控制器的双线冗余控制模块的建模和形式化验证为例,证明了该方法的有效性。

Embedded real-time system has a highly demand in timing constraint,safety and reliability,but traditional methodologies are incapable of modeling and formal verification about the real-time property and safety of system. This paper proposed real-time coloured Petri net model by extending the timing attribute of coloured Petri net so that could simulate and evaluate the timing property of system. According to the transformation rules from real-time coloured Petri net to timed automation,could complete model transformations and could formally verity real-time property,safety and reliability of system using timed computation tree logic. As a conformation of its validity,the described methodology had been successfully applied to modeling and formal verification of line redundancy control unit of train network controller device.