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.
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.
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.
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:
- A graphical system editor allowing graphical descriptions of systems.
- A graphical simulator which provides graphical visualization and recording of the possible dynamic behaviors of a system description, i.e. sequences of symbolic states of the system. It may also be used to visualize traces generated by the model-checker. Since version 3.4 the simulator can visualize a trace as a message sequence chart (MSC).
- A requirement specification editor that also constitutes a graphical user interface to the verifier of Uppaal2k.
- A model-checker for automatic verification of safety and bonded-liveness properties by reachability analysis of the symbolic state-space. Since version 3.2 it can also check liveness properties.
- Generation of diagnostic traces in case verification of a particular real-time system fails. The diagnostic traces may be automatically loaded and graphically visualized using the simulator. Since version 3.4 it is possible to specify that the generated trace should be the shortest or the fastest.