SYNTHESIS AND PROPERTY ANALYSIS OF EMBEDDED SYSTEM MODEL BASED ON PETRI NET WITH INHIBITION ARCS
In order to meet the modeling requirements of embedded system effectively,the embedded system model based on Petri net with inhibition arcs is proposed.However,the PIRES+encountered the"state space explosion"problem when modeling the large-scale complex embedded systems.In order to effectively alleviate this problem,this paper proposed two kinds of synthesis methods of PIRES+,and the preservation of liveness and boundedness of the synthesis net were investigated.The modeling and analysis of the network communication system of a mobile terminal was taken as an example to show the effectiveness of the proposed synthesis methods.
Petri netSystem modelingInhibition arcsSynthesisLiveness