UPPAAL—a Tool Suite for Automatic Verification of Real–Time Systems

Abstract

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 verification 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.