This paper provides an overview of UPPAAL, a tool box for modeling, simulation, and verification of real-time systems. Developed by Uppsala University and Aalborg University, UPPAAL is designed for systems with non-deterministic processes, finite control structures, and real-valued clocks. The tool supports reachability analysis and invariant checking by exploring the state-space of a system using symbolic states and constraint-solving techniques. Key features include an efficient model-checker, on-the-fly searching, and automatic diagnostic traces for debugging. The paper covers the overall structure, design criteria, main components, and user guide for UPPAAL, along with a detailed description of its syntax, semantics, and logic. It also includes a review of case studies and references to the theoretical foundation.This paper provides an overview of UPPAAL, a tool box for modeling, simulation, and verification of real-time systems. Developed by Uppsala University and Aalborg University, UPPAAL is designed for systems with non-deterministic processes, finite control structures, and real-valued clocks. The tool supports reachability analysis and invariant checking by exploring the state-space of a system using symbolic states and constraint-solving techniques. Key features include an efficient model-checker, on-the-fly searching, and automatic diagnostic traces for debugging. The paper covers the overall structure, design criteria, main components, and user guide for UPPAAL, along with a detailed description of its syntax, semantics, and logic. It also includes a review of case studies and references to the theoretical foundation.