Simulation techniques for proving properties of real-time systems

Abstract

The method of simulations is an important technique for reasoning about real-time and other timing-based systems. It is adapted from an analogous method for untimed systems. This paper presents the simulation method in the context of a very general automaton (i.e., labelled transition system) model for timing-based systems. Sketches are presented of several typical examples for which the method has been used successfully. Other complementary tools are also described, in particular, inv’~riants for safety proofs, progress functions for timing proofs, and execution correspondences for liveness proofs.