View article

Model checking is a powerful technique for the automatic verification of finite-state systems [10, 13, 8]. A model-checking algorithm determines whether a finite-state system, represented by its' state-transition graph, satisfies its specification given as a temporM logic formula. For speed independent or delay insensitive systems, the correctness can be proved by abstracting away real-time retMning only the sequencing of state-transitions. For such systems, model checking has a long history spanning over ten years, and has been shown to be useful in validating protocols and circuits [7]. Only recently there have been attempts to extend these techniques to verification of timing properties that explicitly depend upon the actual magnitudes of the delays [15, 4, 2, 1, 18, 3]. Because of the practical need for some support for developing reliable real-time systems, the interest in studying these techniques further is …