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.
TAC95.ps (286k, postscript) OR TAC95.zip (90k, zipped postscript)
TAC95.ps.Z (116k, compressed postscript) OR TAC95.dvi.gz (54k, gzipped dvi)
@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}, }