Skip to main content.

New Features

UPPAAL 4.0 is the result of over 2 years of development. It is more user friendly, has more features and is faster than UPPAAL 3.4. The following is a summary of the most important improvements.

Performance

Runtime and memory consumption has been reduced. For some models, a drastic reduction is obtained, whereas for other models runtime is comparable to UPPAAL 3.4.

  • New and improved abstractions provide dramatic performance improvements for some models.
  • Memory management has been improved, giving a typical reduction of a factor of 3 to 5 in memory consumption. This does come at a minor cost in performance.
  • The generalised sweep-line method has been implemented in UPPAAL. To use this feature, you need to define one or more progress measures.
  • Symmetry reduction.

Language

The modelling language has been extended with new data types and user defined functions. At the same time a number of inconsistencies have been eliminated in the language. As a consequence most UPPAAL 3.4 models need minor adjustments in order to work with UPPAAL 4.0.

The GUI can convert most UPPAAL 3.4 models to the new syntax automatically. Both the command line utility and the GUI recognize the UPPAAL_OLD_SYNTAX environment variable. Defining this variable switches UPPAAL 4.0 into a compatibility mode, in which the 3.4 syntax is recognized. This option may also be of use with third party tools that generate UPPAAL models and execute UPPAAL as a backend.

The following is a summary of the language changes.

  • New types:
    • Record types.
    • Type declarations.
    • Meta variables.
    • Scalars.
  • Partial instantiation of process templates.
  • Comparison and assignment between arrays.
  • User defined functions.
  • Forall and exist quantifiers.
  • Non-deterministic choice on edges.
  • Minor adjustments to more closely follow the syntax of C/C++/Java, including:
    • Declaration of constants.
    • Assignment operator changed from := to =.
    • Explicit declaration of whether parameters use call by value and call by reference semantics.

Graphical User Interface

A number of long standing issues in the graphical user interface have been fixed. Although we feel that the improvements greatly enhance the user experience, most of the changes are minor.

  • The editor now has unlimited undo and redo.
  • Syntax and bracket highlighting.
  • Rectangular selection.
  • Restructured menu layout.
  • Better recovery from fatal server errors.
  • Improved Mac OS X support.
  • Custom colors on locations and edges.
  • Comments can be added to locations and edges.
  • More model checking options are available in the GUI.
  • A search component for the help system was added.
  • Most labels of an automaton can be hidden.
  • Tooltips are used in the declaration editor and automaton editor to show syntax errors. Tooltips also show useful information about locations and edges.

Command Line Interface

The command line interface of verifyta has been updated.

  • More freedom in choice of extrapolation.
  • Can generate pre-stable traces.
  • Can generate fastest concrete traces and concrete traces to deadlocks.
  • Can show statistics about the state space.
  • Can compile a UPPAAL model to a stack-machine program. This is useful as a preprocessor for alternative verification backends.