UPPAAL - now, next, and future

Tobias Amnell, Gerd Behrmann, Johan Bengtsson, Pedro R. D'Argenio, Alexandre David, Ansgar Fehnker, Thomas Hune, Bertrand Jeannet, Kim G. Larsen, M. Oliver Möller, Paul Pettersson, Carsten Weise, Wang Yi

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contributionpeer-review


Uppaal is a tool for modeling, simulation and verification of real-time systems, developed jointly by BRICS at Aalborg University and the Department of Computer Systems at Uppsala University. The tool is appropriate for systems that can be modeled as a collection of non-deterministic processes with finite control structure and real-valued clocks, communicating through channels or shared variables. Typical application areas include real-time controllers and communication protocols, in particular those where timing aspects are critical.

This paper reports on the currently available version and summarizes developments during the last two years. We report on new directions that extends Uppaal with cost-optimal exploration, parametric modeling, stop-watches, probablistic modeling, hierachical modeling, executable timed automata, and a hybrid automata animator. We also report on recent work to improve the efficiency of the tool. In particular, we outline Clock Difference Diagrams (CDDs), new compact representations of states, a distributed version of the tool, and application of dynamic partitioning.

Uppaal has been applied in a number of academic and industrial case studies. We describe a selection of the recent case studies.
Original languageEnglish
Title of host publicationModeling and Verification of Parallel Processes
Subtitle of host publication4th Summer School, MOVEP 2000 Nantes, France, June 19-23, 2000, Revised Tutorial Lectures
EditorsFranck Cassez, Claude Jard, Brigitte Rozoy, Mark Dermot Ryan
Place of PublicationBerlin
PublisherSpringer, Springer Nature
Number of pages26
ISBN (Print)9783540427872, 3540427872
Publication statusPublished - 2001
Externally publishedYes

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


Dive into the research topics of 'UPPAAL - now, next, and future'. Together they form a unique fingerprint.

Cite this