基于Time Petri Nets的实时系统资源冲突检测

Real-Time System Resource Conflict Checking Based on Time Petri Nets

Time Petri Nets在实时系统的建模和性能分析中得到广泛应用,而冲突是Petri网及其扩展模型的重要行为,解决冲突是正确分析模型动态行为的关键.目前随机Petri网、混合Petri网和区间速率连续Petri网的冲突检测方法由于没有考虑到时间约束因此无法在TPN网中使用.时间约束的引入使得Time Petri Nets模型的使能和触发语义比Petri网模型的语义复杂,冲突检测变得更加困难.为了计算冲突发生的时间和概率,首先根据时间约束,给出了变迁持续使能时延迟区间的计算方法,并证明了该方法的合理性和完备性;然后在此基础上定义并证明了Time Petri Nets模型中不冲突的检测方法;并提出了Time Petri Nets模型的冲突检测方法,给出了冲突时间区间和变迁实施概率的计算方法;最后通过实例验证说明了该方法的正确性和有效性.

Time Petri net is widely used to model real-time systems and to analyze system performance. Conflicts are important behaviors of Petri net and its expansion model. To solve conflicts is a key for analyzing model dynamic behaviors. Now, some conflict checking approaches are provided to check conflicts of some expansion Petri Nets which include stochastic Petri Nets, hybrid Petri net （HPN） and interval speed continuous Petri Nets（ICPN）. But these approaches can not be used to check conflicts of time petri nets. Because time constraints are imported, then time Petri net＇s enabling and triggering semantics are more complex than that of Petri net, and the conflict checking of time Petri net is more difficult than that of Petri net. For accurately calculating time intervals and probabilities of conflicts, delay time intervals of transitions are defined based on time constraints when transitions are durative enabling, and the soundness and completeness of this definition are discussed. An approach is proposed to check resources conflicts of time Petri Nets based on time and resource constraints. The approach availability is verified by an example analysis. The results show that applying the approach to check the resource conflicts of real-time systems based on time Petri net modeling is accurate and feasible.