UPPAAL is a tool suite for automatic verification of safety and
bounded liveness properties of real-time systems modeled as networks
of timed automata ~\cite{wpd:forte94,lpw:rtss95,bllpw:dimacs95},
developed during the past two years.  In this paper, we summarize the
main features of UPPAAL in particular its various extensions
developed in 1995 as well as applications to various case-studies,
review and provide pointers to the theoretical foundation.