Property Preservation of Petri Synthesis Net Based Representation for Embedded Systems  

作　　者：Chuanliang Xia Chengdong Li 

机构地区：[1]School of Computer Science and Technology,Shandong Jianzhu University,Jinan 250101,China [2]School of Information and Electrical Engineering,Shandong Jianzhu University,Jinan 250101,China

出　　处：《IEEE/CAA Journal of Automatica Sinica》2021年第4期905-915,共11页自动化学报（英文版）

基　　金：financially supported by the National Natural Science Foundation of China(61503220);the Natural Science Foundation of Shandong Province(ZR2016FM19);the Taishan Scholar Project of Shandong Province(TSQN201812092);the Key Research and Development Program of Shandong Province(2019GGX101072,2019JZZY010115,2018GGX106006);the Youth Innovation Technology Project of Higher School in Shandong Province(2019KJN005)。

摘　　要：Embedded systems have numerous applications in everyday life.Petri-net-based representation for embedded systems(PRES+)is an important methodology for the modeling and analysis of these embedded systems.For a large complex embedded system,the state space explosion is a difficult problem for PRES+to model and analyze.The Petri net synthesis method allows one to bypass the state space explosion issue.To solve this problem,as well as model and analyze large complex systems,two synthesis methods for PRES+are presented in this paper.First,the property preservation of the synthesis shared transition set method is investigated.The property preservation of the synthesis shared transition subnet set method is then studied.An abstraction-synthesis-refinement representation method is proposed.Through this representation method,the synthesis shared transition set approach is used to investigate the property preservation of the synthesis shared transition subnet set operation.Under certain conditions,several important properties of these synthetic nets are preserved,namely reachability,timing,functionality,and liveness.An embedded control system model is used as an example to illustrate the effectiveness of these synthesis methods for PRES+.

关 键 词：Modeling Petri nets property preservation SUBNET SYNTHESIS 

分 类 号：TP301.1[自动化与计算机技术—计算机系统结构] TP368.1[自动化与计算机技术—计算机科学与技术]