Skip to main content.

This page’s menu:

Introduction

Uppaal is an integrated tool environment for modeling, simulation and verification of real-time systems, developed jointly by Basic Research in Computer Science at Aalborg University in Denmark and the Department of Information Technology at Uppsala University in Sweden. It 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 [WPD94, LPW97b]. Typical application areas include real-time controllers and communication protocols in particular, those where timing aspects are critical.

UPPAAL editor

Figure 1: The editor in the Uppaal GUI.

Uppaal consists of three main parts: a description language, a simulator and a model-checker. The description language is a non-deterministic guarded command language with data types (e.g. bounded integers, arrays, etc.). It serves as a modeling or design language to describe system behavior as networks of automata extended with clock and data variables. The simulator is a validation tool which enables examination of possible dynamic executions of a system during early design (or modeling) stages and thus provides an inexpensive mean of fault detection prior to verification by the model-checker which covers the exhaustive dynamic behavior of the system. The model-checker can check invariant and reachability properties by exploring the state-space of a system, i.e. reachability analysis in terms of symbolic states represented by constraints.

UPPAAL simulator

Figure 2: The simulator in the Uppaal GUI. The MSC view in the lower right part is a new feature in Uppaal 3.4.

The two main design criteria for Uppaal have been efficiency and ease of usage. The application of on-the-fly searching technique has been crucial to the efficiency of the Uppaal model-checker. Another important key to efficiency is the application of a symbolic technique that reduces verification problems to that of efficient manipulation and solving of constraints [ WPD94, LPW95c, LLPW97, BLPWW99 ]. To facilitate modeling and debugging, the Uppaal model-checker may automatically generate a diagnostic trace that explains why a property is (or is not) satisfied by a system description. The diagnostic traces generated by the model-checker can be loaded automatically to the simulator, which may be used for visualization and investigation of the trace.

UPPAAL verifier

Figure 3: The verifier in the Uppaal GUI.

Since its first release in 1995, Uppaal has been applied in a number of case studies (see section Case Studies). To meet requirements arising from the case studies, the tool has been extended with various features. The current version of Uppaal, called Uppaal2k, was first released in September 1999. It is a client/server application implemented in Java and C++, and is currently available for Linux, SunOS and Windows 95/98/NT. The features of Uppaal2k include:


Team

Uppaal is developed in collaboaration between the Department of Information Technology at Uppsala University (UPP) in Sweden and the Department of Computer Science at Aalborg University (AAL) in Denmark, with input from several other universites around the world.

The people involved with development and application are Kim G. Larsen (Professor, AAL), Wang Yi (Professor, UPP), Paul Pettersson (Professor, Mälardalen University), Alexandre David (Associate Professor, AAL), Brian Nielsen (Associate Professor, AAL), Arne Skou (Associate Professor, AAL), John Håkansson (Ph.D. Student, UPP), Jacob Illum Rasmussen (Ph.D. Student, AAL), Pavel Krcál (Ph.D. Student, UPP), Ulrik Larsen (Ph.D. Student, AAL), Marius Mikucionis (Ph.D. Student, AAL), and Leonid Mokrushin (Ph.D. Student, UPP).

External contributors include (not complete): Patricia Bouyer (CNRS & ENS de Cachan), Martijn Hendriks (University of Nijmegen), and Radek Pelanek (Masaryk University Brno).

Former members of the development team include (not complete): Gerd Behrmann (AAL), Tobias Amnell (UPP), Johan Bengtsson (UPP), Elena Fersman (UPP), Emmanuel Fleury (AAL), Thomas Hune (Aarhus Univ.), Kåre J. Kristoffersen (AAL), Fredrik Larsson (UPP), Didier Lime (AAL), Oliver Möller (Aarhus Univ.), Justin Pearson (UPP), Carsten Weise (Ericsson), Rune G. Madsen (AAL), and Steffen K. Mortensen (AAL).