This paper presents the overall structure, the design criteria, and the
main features of the tool box \uppaal. It gives a detailed user guide
which describes how to use the various tools of \uppaal\ version 2.02
to {\sl construct} abstract models of a real-time system, to {\sl
simulate} its dynamical behavior, to {\sl specify} and {\sl verify}
its safety and bounded liveness properties in terms of its model. 
%
In addition, the paper also provides a short review on case-studies
where \uppaal\ is applied, as well as references to its theoretical
foundation.