Property Preservation of Object-Oriented Petri Reduction Net Based Representation for Embedded Systems

Embedded systems are widely used in automotive electronics, smart home, smart medical, aerospace and other fields. Aiming at the problem of formal modeling and verification analysis of embedded systems, a solution is proposed using extended Petri net reduction operations. Petri net based representation for embedded system (PRES+) and the object-oriented technology are combined to obtain the object-oriented PRES+ (OOPRES+). Two kinds of subnet reduction rules of OOPRES+ are presented. The preservation of boundedness and liveness of the reduction net system has been investigated to alleviate the problem of state space explosion of OOPRES+. The modeling and analysis of the embedded control system of a smart restaurant is used as an example to verify the effectiveness of the subnet reduction rules. Results obtained can provide an effective way to examine the reduction property of Petri net systems, and present a powerful means to model and verify the large-scale complex embedded systems.

Automated summary

Embedded systems are widely used in various fields such as automotive electronics, smart home, smart medical, and aerospace. This study presents a solution for the formal modeling and verification analysis of embedded systems using extended Petri net reduction operations. The object-oriented PRES+ (OOPRES+) is obtained by combining Petri net based representation for embedded system (PRES+) with object-oriented technology. Two kinds of subnet reduction rules of OOPRES+ are introduced to alleviate the problem of state space explosion. The effectiveness of these rules is verified through the modeling and analysis of an embedded control system in a smart restaurant.