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 for representing and transforming networks of timed automata, a compiler for converting linear hybrid systems into timed automata, and a model-checker based on constraint-solving techniques. UPPAAL also supports diagnostic model-checking, providing diagnostic information when verification fails. The current version is available online. UPPAAL was developed through collaboration between BRICS at Aalborg University and the Department of Computer Systems at Uppsala University. The tool is implemented in C++ and addresses state-explosion problems using on-the-fly verification and symbolic techniques. Key features include a graphical interface based on Autograph, automatic compilation of graphical definitions into textual format, analysis of hybrid automata, syntactical checks before verification, and generation of diagnostic traces. The paper presents UPPAAL's features, theoretical foundation, and applications to case studies. UPPAAL's main features include the ability to draw networks of timed automata using Autograph, automatic compilation, analysis of hybrid automata, syntactical checks, and diagnostic trace generation. The system is designed for efficiency and ease of use.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 for representing and transforming networks of timed automata, a compiler for converting linear hybrid systems into timed automata, and a model-checker based on constraint-solving techniques. UPPAAL also supports diagnostic model-checking, providing diagnostic information when verification fails. The current version is available online. UPPAAL was developed through collaboration between BRICS at Aalborg University and the Department of Computer Systems at Uppsala University. The tool is implemented in C++ and addresses state-explosion problems using on-the-fly verification and symbolic techniques. Key features include a graphical interface based on Autograph, automatic compilation of graphical definitions into textual format, analysis of hybrid automata, syntactical checks before verification, and generation of diagnostic traces. The paper presents UPPAAL's features, theoretical foundation, and applications to case studies. UPPAAL's main features include the ability to draw networks of timed automata using Autograph, automatic compilation, analysis of hybrid automata, syntactical checks, and diagnostic trace generation. The system is designed for efficiency and ease of use.