Property Analysis of Gateway Refinement of Object-Oriented Petri Net with Inhibitor-Arcs-Based Representation for Embedded Systems

This paper focuses on embedded system modeling, proposing a solution to obtain a refined net via the refinement operation of an extended Petri net. Object-oriented technology and Petri net with inhibitor-arcs-based representation for embedded systems (PIRES+) are combined to obtain an object-oriented PIRES+ (OOPIRES+). A gateway refinement method of OOPIRES+ is proposed, and the preservation of the liveness, boundedness, reachability, functionality, and timing of the refined net system is investigated. The modeling analysis of a smart home system is taken as an example to verify the effectiveness of the refinement method. The results can provide an effective way for the investigation of the refined properties of a Petri net system and a favorable means for large-scale complex embedded system modeling, which has broad application prospects.