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 Timed Transition Models (TTM’s), which is introduced along with our adaptation of Milner’s 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.