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 co...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+.展开更多
基金financially supported by the National Natural Science Foundation of China(61503220)the Natural Science Foundation of Shandong Province(ZR2016FM19)+2 种基金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+.
