[an error occurred while processing this directive]

UPPAAL 3.4 Release Info

UPPAAL 3.4.0 is a new stable release of UPPAAL and can be downloaded from the UPPAAL web site.

Compared to the 3.2 release, this release features performance improvements, language improvements, and user interface improvements. Each will be considered in detail in the following.

Runtime Requirements

UPPAAL 3.4 requires the Java Runtime Environment version 1.4.0 or newer. One of the following operating systems is required:

Some users have reported success running Uppaal on FreeBSD, but this platform is not officially supported. Also, it should be possible to run the GUI on any platform supported by the Java Runtime Envionrment 1.4.0 or newer, but the verification engine is not supported on other platforms than those listed above.

Performance Improvements

The core verification engine has once again been reworked and features improved memory management and modularity. Combined with major changes in the internal data structures and minor tweaks in various algorithms, this has lead to much improved performance.

Detailed list of major changes:

Language Improvements

We are currently moving to a new language for UPPAAL 4.0, which will feature a nice subset of the C programming language. We will keep the automata based interface, but add the ability to use C data types and C expressions including calls to user defined functions, which are evaluated as atomic statements (thus eliminating one of the uses of committed locations). Most of the new parser library has been implemented (see libutap for more information on the library) and is used in a restricted mode in the 3.4 release.

The language in UPPAAL 3.4 is a superset the language in UPPAAL 3.2, i.e. every valid 3.2 file should also be a valid 3.4 file (there are a few exceptions, which we consier bugs in the 3.2 parser). A number of features from the 4.0 language have been enabled in 3.4. This includes multi dimensional arrays, arrays of constants, channels and clocks (in addition to arrays of integers), array initialisers, booleans, and C expressions (with the exception of binary negation).

Finally, a new broadcast channel type has been added (non-blocking one-to-many communication).

One important change is the interpretation of out-of-range assignments. UPPAAL 3.2 uses a "wrap-arround" semantics, e.g. when assigning the value 10 to a variable with range [0,3] the result would be 2. One can argue, that this is not always the intended behaviour, and if it is it should be explicitly incorporated into the model rather than handled by the verification engine. Therefore we now consider such assignments invalid. In case of invalid assignments (or other invalid operations like out-of-range array lookups and division by zero), the successor is pruned from the state-space (since it is not well-defined). The command line tool can produce warnings whenever this happens. At the moment there is no way to get access to these warnings from the graphical users interface (this will be fixed in a future version).

Detailed list of major changes:

User Interface Improvements

In UPPAAL 3.4, the graphical user interface has gotten a face lift. Besides a new tool bar and new icons, the editor component has been rewritten, featuring anti-aliasing, curved edges, and a new interaction pattern. Also, a list of all syntax errors is shown directly in the editor, thus making it much easier to get an overview of errors.

The simulator reuses the new rendering component. It also features a new message sequence chart view of the trace loaded, making it easy to analyse the communication structure of the model. Selecting one of the enabled transitions in the simulator now restricts the zone of the state to those points were the transition is enabled.

The verifier can generate shortest (in number of edges) and fastest (in terms of model time) diagnostic traces. This is a back port of some of the features of the unofficial cost optimising version of UPPAAL.

Finally, the command line tool (verifyta) is now able to read TA, XTA and XML files directly. Thus there is no need for the TA format anymore and the "Save As TA file" feature has been deprecated. Notice that the XTA format is a superset of the TA format, and users preferring to create models directly in the TA format can simply use the XTA format and get all the benefits of the template mechanism.

Detailed list of major changes: