DocumentCode :
2266471
Title :
A transformational method for verifying safety properties in real-time systems
Author :
Franklin, M.K. ; Gabrielian, Armen
Author_Institution :
Thomson-CSF Inc., Palo Alto, CA, USA
fYear :
1989
fDate :
5-7 Dec 1989
Firstpage :
112
Lastpage :
123
Abstract :
A two-step method is presented for verifying that safety properties are not violated by an HMS (hierarchical multistate) specification of a system. In the first step, the question of safety verification is recast as a reachability problem in an extension of the HMS machine. In the second step, reachability is determined by the use of correctness-preserving and partial correctness-preserving transformations. The method is shown to be complete, and it is illustrated by verifying that a safety property holds for a simple railroad-crossing system if all of its deadlines are met
Keywords :
finite automata; real-time systems; hierarchical multistate specification; partial correctness-preserving transformations; railroad-crossing system; reachability problem; real-time systems; safety properties verification; transformational method; two-step method; Automata; Logic; Petri nets; Programming; Protocols; Railway safety; Real time systems; Road safety; Software standards; Standards development;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Real Time Systems Symposium, 1989., Proceedings.
Conference_Location :
Santa Monica, CA
Print_ISBN :
0-8186-2004-8
Type :
conf
DOI :
10.1109/REAL.1989.63562
Filename :
63562
Link To Document :
بازگشت