UPPAAL is a tool box for modeling, simulation, and verification of real-time systems. It is based on constraint-solving and on-the-fly techniques, developed jointly by Uppsala University and Aalborg University. UPPAAL is suitable for systems that can be modeled as a collection of non-deterministic processes with finite control structure and real-valued clocks, communicating through channels and/or shared variables. It is mainly designed to check invariant and reachability properties by exploring the state-space of a system. The two main design criteria for UPPAAL are efficiency and ease of usage. The restriction to reachability analysis has been crucial to the efficiency of the UPPAAL model-checker. Another important key to efficiency is the application of on-the-fly searching techniques combined with the symbolic technique that reduces verification problems to that of manipulating and solving simple constraints. UPPAAL provides a detailed user guide which describes how to use the various tools of UPPAAL version 2.02 to construct abstract models of a real-time system, to simulate its dynamical behavior, to specify and verify its safety and bounded liveness properties in terms of its model. The paper also provides a short review on case-studies where UPPAAL is applied, as well as references to its theoretical foundation. UPPAAL consists of three main parts: a description language, a simulator, and a model-checker. The description language is a non-deterministic guarded command language with data types. It serves as a modeling or design language to describe system behavior as networks of timed automata extended with data variables. The simulator and the model-checker are designed for interactive and automated analysis of system behavior by manipulating and solving constraints that represent the state-space of a system description. They have a common basis, i.e., constraint-solvers. The simulator enables examination of possible dynamic executions of a system during early modeling (or design) stages and thus provides an inexpensive mean of fault detection prior to verification by the model-checker which covers the exhaustive dynamic behavior of the system. UPPAAL provides both graphical and textual formats for the description language. The textual format (i.e., .ta) provides a basic programming language for timed automata. The compiler atg2ta automatically transforms system description in the graphical .atg-format into the textual .ta-format, thus supporting the important principle WYSIWYV. The UPPAAL description language also supports modeling of simple linear hybrid automata.UPPAAL is a tool box for modeling, simulation, and verification of real-time systems. It is based on constraint-solving and on-the-fly techniques, developed jointly by Uppsala University and Aalborg University. UPPAAL is suitable for systems that can be modeled as a collection of non-deterministic processes with finite control structure and real-valued clocks, communicating through channels and/or shared variables. It is mainly designed to check invariant and reachability properties by exploring the state-space of a system. The two main design criteria for UPPAAL are efficiency and ease of usage. The restriction to reachability analysis has been crucial to the efficiency of the UPPAAL model-checker. Another important key to efficiency is the application of on-the-fly searching techniques combined with the symbolic technique that reduces verification problems to that of manipulating and solving simple constraints. UPPAAL provides a detailed user guide which describes how to use the various tools of UPPAAL version 2.02 to construct abstract models of a real-time system, to simulate its dynamical behavior, to specify and verify its safety and bounded liveness properties in terms of its model. The paper also provides a short review on case-studies where UPPAAL is applied, as well as references to its theoretical foundation. UPPAAL consists of three main parts: a description language, a simulator, and a model-checker. The description language is a non-deterministic guarded command language with data types. It serves as a modeling or design language to describe system behavior as networks of timed automata extended with data variables. The simulator and the model-checker are designed for interactive and automated analysis of system behavior by manipulating and solving constraints that represent the state-space of a system description. They have a common basis, i.e., constraint-solvers. The simulator enables examination of possible dynamic executions of a system during early modeling (or design) stages and thus provides an inexpensive mean of fault detection prior to verification by the model-checker which covers the exhaustive dynamic behavior of the system. UPPAAL provides both graphical and textual formats for the description language. The textual format (i.e., .ta) provides a basic programming language for timed automata. The compiler atg2ta automatically transforms system description in the graphical .atg-format into the textual .ta-format, thus supporting the important principle WYSIWYV. The UPPAAL description language also supports modeling of simple linear hybrid automata.