New Features

Statistical Model Checking

Stochastic semantics is given to UPPAAL timed automata models and probabilities can be estimated by gathering statistics about simulated runs.

Statistical model checking is facilitated by the following concepts:

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.

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.

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.

Command Line Interface

The command line interface of verifyta has been updated.