Title :
Equivalence preserving transformations for timed transition models
Author :
Lawford, M. ; Wonham, W.M.
Author_Institution :
Dept. of Electr. Eng., Toronto Univ., Ont., Canada
Abstract :
A modified version of Ostroff´s (1989, 1990) timed transition models (TTMs), along with the author´s adaptation of Milner´s (1980, 1989) observation equivalence to TTMs, is introduced. An informal set of `behavior preserving´ transformations is developed. It is shown to be consistent for proving observation equivalence, and is applied to solve an industrial real-time software verification problem. The incompleteness of a given set of transformations is briefly discussed
Keywords :
formal logic; program verification; equivalence-preserving transformations; incompleteness; observation equivalence; real-time software verification; timed transition models; Computer industry; Computer science; Control system synthesis; Control systems; Electrical equipment industry; Equations; Logic; Petri nets; Real time systems; Safety; Time to market;
Conference_Titel :
Decision and Control, 1992., Proceedings of the 31st IEEE Conference on
Conference_Location :
Tucson, AZ
Print_ISBN :
0-7803-0872-7
DOI :
10.1109/CDC.1992.371016
