DocumentCode
2403662
Title
Equivalence preserving transformations for timed transition models
Author
Lawford, M. ; Wonham, W.M.
Author_Institution
Dept. of Electr. Eng., Toronto Univ., Ont., Canada
fYear
1992
fDate
1992
Firstpage
3350
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Decision and Control, 1992., Proceedings of the 31st IEEE Conference on
Conference_Location
Tucson, AZ
Print_ISBN
0-7803-0872-7
Type
conf
DOI
10.1109/CDC.1992.371016
Filename
371016
Link To Document