An Automatic Verification Technique for Communicating Real-Time State Machines

We describe an automatic verification technique for distributed real-time systems that are specified as Communicating Real-Time State Machines (CRSMs). CRSMs are timed state machines that communicate synchronously over uni-directional channels. The proposed approach is to model the behavior of the system of (an expressive subclass of) CRSMs by a timed reachability graph. The system behavior of CRSMs is characterized by a time-stamped trace of communication events. We provide a decision procedure for verifying timing and safety properties (specified in a notation based on Real-Time Logic) of the reachability graph, and hence of the corresponding system of CRSMs. We also present a condition for the existence of deadlock in a system of CRSMs. Finally, we briefly describe an implementation of a verifier program based on the above algorithms. Keywords --- automatic verification, deadlock, model checking, reachability, real-time, requirements specification. 1 Introduction The distinguishin..