计算机科学与探索 ›› 2008, Vol. 2 ›› Issue (6): 614-626.DOI: 10.3778/j.issn.1673-9418.2008.06.005

• 学术研究 • 上一篇    下一篇

基于Petri网表示的嵌入式系统模型化简规则

夏传良1,2+   

  1. 1. 山东建筑大学 计算机学院,济南 250101
    2. 中国科学院软件研究所 计算机科学国家重点实验室,北京 100190
  • 收稿日期:1900-01-01 修回日期:1900-01-01 出版日期:2008-12-06 发布日期:2008-12-06
  • 通讯作者: 夏传良

Reduction rules for Petri Net based representation for embedded systems

XIA Chuanliang1,2+   

  1. 1. School of Computer Science and Technology, Shandong Jianzhu University, Jinan 250101, China
    2. State Key Laboratory for Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100190, China
  • Received:1900-01-01 Revised:1900-01-01 Online:2008-12-06 Published:2008-12-06
  • Contact: XIA Chuanliang

摘要: 为了提高基于Petri网表示的嵌入式模型(PRES+)验证的效率, 对模型进行了保性变换, 给出了一组关于PRES+模型的化简规则, 这些化简规则在原模型和简化模型之间保持完全等价关系。对两个系统模型的化简结果进一步说明了这些化简规则的有效性。

关键词: 化简规则, Petri网, 完全等价, 保性, 嵌入式系统

Abstract: The research concentrates on the aspects related to reduction rules for Petri Net based Representation for Embedded Systems (PRES+). The major motivation of this work is to give correctness-preservation transformations to improve the verification efficiency. It proposes a set of reduction rules to reduce PRES+ nets to the equivalent reduced PRES+ nets. Reductions for two system models demonstrate the efficiency of this reduction rules on practical applications.

Key words: reduction rules, Petri Nets, total-equivalence, property preservation, embedded system