Title :
State-based specification of complex real-time systems
Author :
Gabrielian, A. ; Franklin, M.K.
Author_Institution :
Thompson-CSF Inc., Palo Alto, CA, USA
Abstract :
A state-based specification methodology for real-time systems is presented that reduces the number of states by orders of magnitude compared to standard techniques and provides explicit representation for temporal constraints. Formal definitions and a graphic notation for the associated hierarchical multistate (HMS) machines are presented, and various concepts of hierarchy of HMS machines are explored. A promising approach to reusability of specifications using generic nondeterministic HMS machines is introduced. Some preliminary results are presented on the formal verification of properties of an HMS machine by (1) extending it to represent requirements as new states and (2) performing reachability analysis on the extended machine to prove the consistency of the requirements with the original specification
Keywords :
program verification; real-time systems; complex real-time systems; formal verification; graphic notation; hierarchical multistate; reachability analysis; reusability; state-based specification methodology; temporal constraints; Clocks; Concurrent computing; Delay effects; Formal verification; Graphics; Logic; Performance analysis; Real time systems; Timing; Vehicle dynamics;
Conference_Titel :
Real-Time Systems Symposium, 1988., Proceedings.
Conference_Location :
Huntsville, AL
Print_ISBN :
0-8186-4894-5
DOI :
10.1109/REAL.1988.51095
