基于Petri的分布式实时嵌入式软件合理性分析

摘要

合理的模型是保证分布式实时嵌入式(DRE)软件可靠性的关键.提出了分析DRE软件模型的合理性方法.该方法基于带抑制弧的时间Petri网(ITPN),采用自顶向下的策略对功能模块及其通信过程分别建模,并利用Petri网的合成运算形成整个应用的ITPN模型.在确保系统实时性的前提下,给出软件模型合理性的形式化定义及其判定定理.最后以实例说明该方法的可行性.