Equivalence preserving transformations for timed transition models

The increasing use of computer control systems in safety-critical real-time systems has led to a need for methods to ensure the correct operation of real-time control systems. Through an example, this paper introduces the use of algebraic equivalence to verify the correct operation of such systems. A controller is considered verified if its implementation is proven to be equivalent to its specification. Real-time systems are modeled using a modified version of Ostroff's (1989, 1990) timed transition models (TTM's), which is introduced along with our adaptation of Milner's (1980, 1989) observation equivalence to TTM's. A set of "behavior preserving" transformations is then developed, shown to be consistent for proving observation equivalence, and applied to solve an industrial real-time controller software verification problem. Finally the incompleteness of a given set of transformations is briefly discussed.<>