HOME    PRODUCT    SOLUTIONS    PARTNERS    SUPPORT    WEB HELP    CONTACT US    ABOUT UP4ALL          

UPPAAL v.4™

 The verification platform


v.4 logo

UPPAAL is an integrated tool environment for modeling, simulation and, verification of real-time embedded systems. Typical application areas of UPPAAL includes real-time controllers and communication protocols in particular, those where timing aspects are critical.

The tool environment

V.4 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. Uppaal v.4 consists of three main parts.

A description language

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

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 model-checker

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.

State of art criterias

UPPAAL v.4 has been developed specifically for the end user in mind by implementing two ideas of concept. They are efficiency and ease of usage. The model-checker has in its on-the-fly searching technique a state of art function which is crucial to the efficiency when a user is modeling, simulating or trying to verificate a result of a real-time system.

Another important key is the application of a symbolic technique that reduces verification problems to that of efficient manipulation and solving of constraints.

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.


Key features of UPPAAL v.4

A graphical system editor allowing graphical descriptions of systems.
A graphical simulator which provides graphical visualization.
A requirement specification editor.
A model-checker for automatic verification.
Generation of diagnostic trace

Frequently asked questions

Latest version is UPPAAL v.4.0.13

This version corrects bugs in the parser and the virtual machine. This update is recommended since certain nested function calls could return wrong results. Click here for more information on this update. 


UPPAAL tutorial

Mailing List

Join the UPPAAL Yahoo forum.


Feedback

Share your feedback with us and help make UPPAAL v.4 even better.