Property preservation of refinement for Petri net based representation for embedded systems

详细信息    查看全文

• 作者：Chuanliang Xia
• 关键词：Petri nets ; Refinement ; Liveness ; Timing ; Property preservation
• 刊名：Cluster Computing
• 出版年：2016
• 出版时间：September 2016
• 年：2016
• 卷：19
• 期：3
• 页码：1373-1384
• 全文大小：731 KB
• 刊物类别：Computer Science
• 刊物主题：Processor Architectures
  Operating Systems
  Computer Communication Networks
  
• 出版者：Springer Netherlands
• ISSN：1573-7543
• 卷排序：19

文摘

Embedded systems have many applications in our life. Petri net based Representation for Embedded Systems (PRES+) is a promising methodology for modeling, verification, analysis and control of embedded systems. But the state space explosion problem is somewhat tedious for PRES+ to specify and analyze large complex embedded systems. To solve state space explosion problem of PRES+, in this work, we concern with a method for expanding PRES+ model to the desired level of detail using refinement. A kind of refinement approach for PRES+ is proposed. We propose definitions of two PRES+ models have the same dynamic properties, such as reachability, timing and functionality. Reachability, timing and functionality preservations of the refined net are investigated. Definitions of liveness and boundedness of PRES+ are presented. We propose conditions under which liveness and boundedness will be preserved by using this refinement approach. A temperature measure and control example illustrates the efficiency of our refinement approach on practical applications. These results can be applied nicely to solve embedded systems design problems.