State-based specification of complex real-time systems

Author

Gabrielian, A. ; Franklin, M.K.

Author_Institution

Thompson-CSF Inc., Palo Alto, CA, USA

fYear

1988

fDate

6-8 Dec 1988

Firstpage

2

Lastpage

11

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Real-Time Systems Symposium, 1988., Proceedings.

Conference_Location

Huntsville, AL

Print_ISBN

0-8186-4894-5

Type

conf

DOI

10.1109/REAL.1988.51095

Filename

51095