Reduction Rules For Petri Net With Inhibitor Arcs Based Representation For Embedded Systems

Embedded systems are widely used in unmanned aerial vehicle,smart homes,medical devices and other fields.High requirements for reliability,correctness,and real-time are the basic characteristics of embedded systems.With the development of embedded technology,the complexity of embedded systems continues to increase and their dependence on time is increasing.In order to ensure the correctness and effectiveness of the system,it is necessary to adopt formal modeling methods in the design of embedded systems.Petri net is a mathematical model for modeling and analyzing the system using intuitive graphics and formal proofs.However,the classic Petri net lacks time characteristics and ability of data expression and it cannot describe the real-time requirements and data flow of embedded systems well.Petri net based Representation for Embedded Systems(PRES+)can be used to describe real-time embedded systems,but it is tedious and unintuitive when modeling complex embedded systems.Aiming at these shortcomings of the classic Petri net and PRES+ net,this paper adds inhibitor arcs to the PRES+ net.Then,Petri net with Inhibitor arcs based Representation for Embedded Systems(PIRES+)is obtained.The PIRES+ net enhances the ability to model and verify complex embedded systems.However,there is a problem of state space explosion in the process of modeling and verifying complex embedded systems.In order to alleviate this problem,the PIRES+ net is simplified and a number of property preservation of reduction rules for the PIRES+ net are proposed,so that the simplified model has the same reachability,real-time,functionality,liveness and boundedness as the original net.The concept of total-equivalence of the PIRES+ net is given and the conditions of the same reachability,functionality and real-time of two PIRES+ net are given.The reduction rule based on series places,the reduction rules based on series transitions,the reduction rules based on places with the same input and output,the reduction rules based on specific transitions and places,the reduction rules based on T-type subnets and P-type subnets are proposed.Under certain constraints,the simplified PIRES+ net has the same reachability,functionality,and real-time performance as the original PIRES+ net.The effectiveness of reduction rules is illustrated by simplification of three application examples.The state concept of PIRES+ net is proposed,and the formal definition of the liveness and boundedness of PIRES+ net is given.Prove that the reduction rules based on P-type subnet and T-type subnet maintain the liveness and boundedness respectively.The analysis and reduction of alarm based on embedded systems illustrate the feasibility and effectiveness of redution rules based on P-type subnet and T-type subnet.Finally,six kinds of reduction rules are systematically applied to multi-parameter monitor system,and the number of storage places and transitions are reduced under the premise of property preservation,which alleviates the state space explosion problem of the net system to a certain extent.