Automatic Verication of Real-time Communicating Systems by Constraint Solving

Abstract. In this paper, an algebra of timed processes with real-valued clocks is presented, which may serve as a description language for networks of timed automata. We show that requirements such as \a process will never reach an undesired state " can be veried by solving a simple class of constraints on the clock-variables. A symbolic on-the- y reachability algorithm for the language has been developed and implemented as a software tool based on constraint-solving techniques. To our knowledge, this is the rst on-the- y verication algorithm for timed automata. In fact, the tool is the very rst implementation of the Uppaal tool. As examples, we model and verify safety properties of a real-time mutual exclusion protocol and a railway crossing controller.