# Equivalence Preserving Transformations for Timed Transition Models

### by M. Lawford and W.M. Wonham

**Abstract:** 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 (TTMs), which is introduced along
with our adaptation of Milner's observation equivalence to TTMs. A
set of ``behavior preserving'' transformations is then developed,
shown to be consistent for proving observation equivalence, and then
applied to solve an industrial real-time controller software
verification problem. Finally the incompleteness of a given set of
transformations is briefly discussed.

### Download

TAC95.ps (286k, postscript)
OR TAC95.zip (90k, zipped postscript)

TAC95.ps.Z (116k, compressed postscript)
OR TAC95.dvi.gz (54k, gzipped dvi)

### BibTeX Entry

@article{LawWon:95,
author = {M. Lawford and W.M. Wonham},
title = {Equivalence Preserving Transformations of Timed
Transition Models},
journal = "IEEE Trans.\ Autom.\ Control",
volume = {40},
pages = {1167--1179},
month = jul,
year = {1995},
}

[
CAS |
ML |
Papers ]