UPPAAL is a tool for the modeling, validation and verification of real-time systems. It is appropriate for systems that can be modeled as a collection of non-deterministic processes with finite control structure and real-valued clocks (i.e., timed automata), communicating through channels and (or) shared data structures. The tool is developed in collaboration between the Department of Information Technology at Uppsala University, Sweden and the Department of Computer Science at Aalborg University, Denmark. It provides a model-checker engine.