A Hierarchical Verification Procedure of Timed Petri-Net Model for Real-Time Embedded Systems

A novel approach to verify the timed Petri-Net model is proposed in this paper. A non-instantaneous model is abstracted from the timed Petri-Net model in a hierarchical structure. The non-instantaneous model which is verified with a model-checking tool is used to reduce the state space of the timed Petri-Net model for verification with a satisfiability modulo theories solver. The proposed approach is applied in verifying the non-functional properties of real-time embedded systems.The timed Petri-Net is used to model the interacting relations of the software components and the binding relations between software and hardware. A platform-independent model which abstracted from the scheduling model is transformed into the non-instantaneous model.The performance evaluation shows the improvement on the running time for verification with the proposed approach.