Synthesis For Petri Net With Inhibitor Arcs Based Representation For Embedded Systems

Since the advent of microprocessor,embedded system has been widely used in all kinds of network and chip technology.Nowadays,embedded system has strong specificity and reliability characteristics.In the early design stage of embedded system,using effective modeling methods to model the system can effectively reduce the errors of system design,therefore it is particularly important to provide an effective modeling method.With the development of embedded system,the traditional Petri net cannot adapt to the current situation of embedded system modeling,therefore Petri net based representation for embedded systems is proposed.Although the proposal of PRES+ expands the application of Petri net in the field of system modeling to a certain extent,the description ability of PRES+ is weak and the description method is complex when describing the priority of tasks in the modeling system.Therefore,the inhibitor arcs are added to PRES+,and the Petri net with inhibitor arcs based representation for embedded systems is obtained.PIRES+ not only has the advantage of timing description of PRES+,but also can use the inhibitor arcs to control the execution sequence of tasks,therefore the PIRES+ can better satisfy the modeling needs of large-scale and complex embedded systems.However,when using PIRES+ to model and analyze large-scale and complex embedded system,the increase of system complexity will lead to the exponential growth of reachable identifiers in Petri net,and then the problem of state space explosion will appear,this problem is a NP hard problem,which cannot be completely solved at this stage.In order to satisfy the modeling requirements of large-scale and complex embedded systems,and effectively alleviate the state space explosion problem,this thesis presents the synthesis operation method of PIRES+.The shared synthesis operation of PIRES+ can effectively alleviate the problem of state space explosion,and make the synthesis PIRES+ preserve the liveness,functionality,timing and other related properties of PIRES+before synthesis.This thesis first briefly introduces the basic definitions of Petri net with inhibitor arcs and PRES+,then leads to the basic definitions of PIRES+,and gives the concepts of transition function,guard function,transition delay,boundedness and other related properties in PIRES+.For different types of PIRES+,the synthesis operation rules of shared transition set and shared transition subnet set are proposed.In order to better study the preservation of the original properties of PIRES+ synthesis,the analysis method of "abstraction-synthesis-refinement" is introduced.According to this analysis method,the accuracy of synthesis rules is verified through formal proof.Finally,through the modeling and analysis of the instantiated embedded system,the feasibility and practicability of the shared synthesis rules proposed in this thesis are verified.