基于DTPN的时间Petri网的组件级化简规则

Component-Level Reduction Rules for Time Petri Nets Based on DTPN

时间Petri网(TPNs)是实时系统时间特性常用的描述和验证的Petri网模型。组件级化简方法是TPN模型常用的分析方法,在保持外部可观察时间特性的前提下,将组件TPN模型化简成一个很简单的TPN模型。然而它却失去了组件内部的性质,如冲突和并发等性质。文中引入延迟时间Petri网(DTPN),通过组件TPN模型向DTPN模型转化,使化简后模型既保持外部可观察时间特性,又保持组件内部的冲突和并发等性质。为了分析化简后的DTPN模型,文中还提出了一种新的DT- PN调度分析方法。最后通过对一个C2系统的组件TPN模型的分析实例,验证该方法的有效性。

Time Petri Nets （TPNs） are a popular Petri net model for specification and verification of real -time systems. A widely applied method for analyzing Petri nets is component - level reduction analysis. The existing technique for component - level reduction analysis transforms a TPN component to a constant size of simple one while maintains the net＇ s external observable timing properties, but it neglects the internal properties of component such as conflict and concurrency. Based on Delay Time Petri Net （DTPN） , the paper transforms a TPN component to DTPN model in order to preserve not only external observable timing properties but also such the internal characters as conflict and concurrency during the reduction. For the sake of analyzing the DTPN model after reduction, the paper proposes a new schedule analysis method. Finally, the method is verified by its application to C2 system.