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 ]