Reachability analysis of real-time systems using time Petri nets

摘要

Time Petri nets (TPNs) are a popular Petri net model fornspecification and verification of real-time systems. A fundamental andnmost widely applied method for analyzing Petri nets is reachabilitynanalysis. The existing technique for reachability analysis of TPNs,nhowever, is not suitable for timing property verification because onencannot derive end-to-end delay in task execution, an important issue forntime-critical systems, from the reachability tree constructed using thentechnique. In this paper, we present a new reachability based analysisntechnique for TPNs for timing property analysis and verification thatneffectively addresses the problem. Our technique is based on a conceptncalled clock-stamped state class (CS-class). With the reachability treengenerated based on CS-classes, we can directly compute the end-to-endntime delay in task execution. Moreover, a CS-class can be uniquelynmapped to a traditional state class based on which the conventionalnreachability tree is constructed. Therefore, our CS-class-based analysisntechnique is more general than the existing technique. We show how tonapply this technique to timing property verification of the TPN model ofna command and control (C2) system