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 oper ation of real-time control systems, Through an example, this paper int roduces the use of algebraic equivalence to verify the correct operati on of such systems, A controller is considered verified if its impleme ntation is proven to be equivalent to its specification. Real-time sys tems are modeled using a modified version of Ostroff's Timed Transitio n Models (TTM's), which is introduced along with our adaptation of Mil ner's observation equivalence to TTM's. A set of ''behavior preserving '' transformations is then developed, shown to be consistent for provi ng observation equivalence, and applied to solve an industrial real-ti me controller software verification problem, Finally the incompletenes s of a given set of transformations is briefly discussed.