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.
展开▼
