UPPAAL is a tool suite for automatic verification of safety and
bounded liveness properties of real-time systems modeled as networks
of timed automata. It includes: a graphical interface that supports
graphical and textual representations of networks of timed automata,
and automatic transformation from graphical representations to textual
format, a compiler that transforms a certain class of linear hybrid
systems to networks of timed automata, and a model-checker which is
implemented based on constraint-solving techniques. UPPAAL also
supports diagnostic model-checking providing diagnostic information in
case verificat ion of a particular real-time systems fails. 

The current version of UPPAAL is available on the World Wide Web via
the Uppaal home page http://www.docs.uu.se/docs/rtmv/uppaal.