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

Soundness Analysis of Distributed Real-time and Embedded Software Based on Petri Nets

作　　者：陈丽琼[1] 邵志清[1] 王秀英[1] 范贵生[1] 

机构地区：[1]华东理工大学计算机科学与工程系,上海200237

出　　处：《计算机科学》2008年第8期277-280,299,共5页Computer Science

基　　金：国家自然科学基金(60373075);上海市科技发展基金(06dz15004-1)的资助

摘　　要：合理的模型是保证分布式实时嵌入式(DRE)软件可靠性的关键。提出了分析DRE软件模型的合理性方法。该方法基于带抑制弧的时间Petri网(ITPN),采用自顶向下的策略对功能模块及其通信过程分别建模,并利用Petri网的合成运算形成整个应用的ITPN模型。在确保系统实时性的前提下,给出软件模型合理性的形式化定义及其判定定理。最后以实例说明该方法的可行性。The soundness of the model is the key issue to guarantee the reliability of distributed real-time embedded （DRE） software. Reasonable determination method of DRE software model is given in this paper. The method is based on time Petri nets with inhibitor arc, using top-down strategy to respectively model functional modules and the communication process. Exploiting the synthesis operations of Petri nets to form the ITPN model of system. Under the premise to meet real-time property, the formal definition and judgment theorem of soundness of distributed real-time embedded software are presented. Finally, an example is given to explain the feasibility of the method.

关 键 词：分布式实时嵌入式软件 PETRI网 建模 合理性 验证 

分 类 号：TP37[自动化与计算机技术—计算机系统结构] TP311.52[自动化与计算机技术—计算机科学与技术]