Timing analysis of real-time distributed systems in CRSM´s and ERL

Author

Bi, Yaodong

Author_Institution

Dept. of Comput. Sci., Scranton Univ., PA, USA

fYear

1994

fDate

26-29 Oct 1994

Firstpage

630

Lastpage

637

Abstract

The paper presents a method for modeling real-time distributed systems and verifying their timing properties. As a modeling tool, communicating real-time state machines (CRSMs) (A.C. Shaw, 1992) are employed with modifications. For a system with a finite number of states, all of the possible execution paths of the system in CRSMs are constructed into a graph called timed reachability graph (TRG). Timing properties of the system are specified in event-based real-time temporal logic (ERL) (H.Y. Chen et al., 1993) and are verified against the timed reachability graph. A verification algorithm is designed. The contribution of the work is the construction of the timed reachability graph and the verification of timing constraints in ERL

Keywords

discrete event simulation; distributed processing; formal logic; formal verification; graph theory; modelling; real-time systems; temporal logic; CRSM; ERL; TRG; communicating real-time state machines; event-based real-time temporal logic; execution paths; real-time distributed systems; timed reachability graph; timing analysis; timing constraint verification; timing properties; verification algorithm; Algorithm design and analysis; Bismuth; Distributed computing; History; Law; Legal factors; Logic; Real time systems; Time to market; Timing;

fLanguage

English

Publisher

ieee

Conference_Titel

Parallel and Distributed Processing, 1994. Proceedings. Sixth IEEE Symposium on

Conference_Location

Dallas, TX

Print_ISBN

0-8186-6427-4

Type

conf

DOI

10.1109/SPDP.1994.346114

Filename

346114