A Graph-Theoretic Approach for Timing Analysis and its Implementation

This paper presents a graph-theoretic algorithm for safety analysis of a class of timing properties in real-time systems which are expressible in a subset of real time logic (RTL) formulas. Our procedure is in three parts: the first part constructs a graph representing the system specification and the negation of the safety assertion. The second part detects positive cycles in the graph using a node removal operation. The third part determines the consistency of the safety assertion with respect to the system specification based on the positive cycles detected. The implementation and an application of this procedure will also be described.