In: IEEE Trans. on Systems, Man, and Cybernetics; B: Cybernetics, Vol. 30, No. 5, pages 725-736. 2000.
Abstract: Time Petri nets (TPNs) are a popular Petri net model for specification and verification of real-time systems. A fundamental and most widely applied method for analyzing Petri nets is reachability analysis. The existing technique for reachability analysis of TPNs, however, is not suitable for timing property verification because one cannot derive end-to-end delay in task execution, an important issue for time-critical systems, from the reachability tree constructed using the technique. This paper presents a new reachability based analysis technique for TPNs for timing property analysis and verification that effectively addresses the problem. The proposed technique is based on a concept called clock-stamped state class (CS-class). With the reachability tree generated based on CS-classes, the end-to-end time delay in task execution can be directly computed. Moreover, a CS-class can be uniquely mapped to a traditional state class based on which the conventional reachability tree is constructed. Therefore, the proposed CS-class based analysis technique is more general than the existing techniques. The paper shows how to apply this technique to timing property verification of the TPN model of a command and control (C2) system.
Keywords: real-time systems, system specification, system verification, time Petri nets.