Uppaal: a Tool Suite for Validation and Verification of Real-Time Systems

The purpose of this document is to provide a complete description of Uppaal, including its theoretical basis and user guide. Uppaal is a tool suite for simulation and verification of real-time systems modeled as networks of automata with clock and data variables. It consists of a graphical interface, a simulator and a model--checker (or analyzer). The graphical interface supports graphical and textual representations of system descriptions (i.e. networks of automata extended with clock and data variables), and automatic transformation from graphical representations to textual format. It also provides a compiler that transforms a certain class of linear hybrid systems to networks of automata. The simulator enables a grphical visualisation of possible dynamic behaviours (execution traces) of a system description allowing for inexpenseive fault detection at an early stage before actual verification is attempted. The model-checker allows automatic verification of safety and bounded--liveness properties, based on constraint-solving techniques. The model-checker also provides diagnostic information in case verification of