- UPPAAL Help
- GUI Reference
- Language Reference
- Command Line Options
- Remote Server
- File Formats
- 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:
- Discrete probabilistic transitions via weighted probabilistic branches.
- Probabilistic delays over continuous time: unbounded time invariants imply exponential probability distribution of leaving the location and bounded time invariants imply uniform probability distribution.
- Clock variable rates can be specified by any integer expression (not just 1 or 0 in case of stop-watches) as an invariant.
- The probabilistic semantics is based on individual choices of competing processes.
- Statistical properties are based on a state formula and in addition the probability distribution over variable values or computation steps is computed.
- The confidence and other parameters can be changed in the statistical parameters menu option.
- Extra statistics can be examined in the histograms and compared in Plot Composer.
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.
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.
- 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
- 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.