基于Time Petri Net的实时系统冲撞检测与消解  

Real-Time Systems Contact Checking and Resolution Based on Time Petri Net

作　　者：周航[1,2] 黄志球[2] 祝义[2,3] 夏良[4] 刘林源[2] 

机构地区：[1]南京航空航天大学民航学院,南京210016 [2]南京航空航天大学计算机科学与技术学院,南京210016 [3]徐州师范大学计算机科学与技术学院,江苏徐州221116 [4]中国人民解放军炮兵学院计算中心,合肥230031

出　　处：《计算机研究与发展》2012年第2期413-420,共8页Journal of Computer Research and Development

基　　金：国家"八六三"高技术研究发展计划基金项目(2009AA010307);中国民用航空总局科技项目(MHRD2007117)

摘　　要：time Petri net(TPN)在实时控制系统的建模中得到广泛应用,而冲撞是Petri网及其扩展模型的重要行为,解决冲撞是正确分析模型动态行为的关键.由于引入时间约束,使得TPN模型的使能和触发语义比Petri网模型的语义复杂,冲撞的检测及消解变得更加困难.首先根据时间约束,给出了变迁持续使能时延迟区间的计算方法,并证明了该方法的正确性;然后在此基础上定义并证明了TPN模型中冲撞的检测方法;给出了冲撞时间区间及修改时间约束的冲撞消解方法;最后通过实例验证说明了该方法的有效性和正确性.Time Petri net is widely used to model real-time control systems. Contacts are important behaviors of Petri net and these expansion models. To solve the contacts is a key of analyzing models dynamic behaviors. Because the time constraints are adhibited, time Petri net enabling and triggering semantics are becoming more complex than Petri net, and contacts checking and resolution are getting more difficult. Time intervals of transitions are defined when these transitions are durably enabled, and this definition correctness is discussed. An approach is proposed to check contacts of time Petri net and a contacts resolution approach based on changing time constraints of transitions is defined and proved. The approach availability is verified by an example analysis. The results show that applying our approach to check the resource contacts of time Petri net is feasible.

关 键 词：时间PETRI网 时间约束 冲撞 检测 消解 

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]