View article

In this paper, an algebra of timed processes with real-valued clocks is presented, which serves as a formal description language for real-time communicating systems. We show that requirements such as “a process will never reach an undesired state” can be verified by solving a simple class of constraint systems on the clock-variables. A complete method for reachability analysis associated with the language is developed, and implemented as an automatic verification tool based on constraint-solving techniques. Finally as examples, we study and verify the safety-properties of Fischer’s mutual exclusion protocol and a railway crossing controller.