Abstract:
n 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.