【摘要】 带抑制弧的时延着色Petri网(Timed Colored Petri Nets with Inhibitor Arcs,TCPNIA)是一种描述实时嵌入式系统的模型。给出了从TCPNIA到时间自动机的结构化转换算法,以利用变迁冲突调解机制保证TCPNIA模型和转换后的时间自动机模型语义等价;并给出了语义等价的证明和算法复杂度分析。层次化方法被用来提高模型检测的时间与空间效率。通过实际案例展示了该技术的应用和可行性。更多还原

【Abstract】 TCPNIA(Timed Colored Petri Nets with Inhibitor Arcs,TCPNIA) is a model for specifying embedded systems.This paper proposed a structural transformation method from TCPNIA to TA(Timed Automata,TA).A collision mediation mechanism was introduced to ensure the semantics equivalence between TCPNIA and the transferred counterpart.The semantics equivalence was proved.The complexity of the transformation algorithm was analyzed.Hierarchical method was utilized to improve time and space efficiency in model checking.A case study shows the applicability and feasibility of the technique.更多还原