Skip to main content.


Figure: Uppaal PORT in SAVE IDE on screen.

Uppaal PORT is a is a new tool for component-based modelling, simulation, and verification of real-time and embedded systems modelled as real-time components. Uppaal PORT can be used used together with the SAVE integrated Development Enviroment (IDE) which is developed as an Eclipse plugin.

Together with SAVE IDE, Uppaal PORT supports graphical modelling of internal component behaviour as Uppaal timed autoamta, and hirerachical composition of components. The simualtor of SAVE IDE allows its users to explore the dynamical behviour of components, and can be used to call the model-checker of Uppaal PORT to verify properties expressed in a subset of timed CTL. The current input file format for Uppaal PORT models is described in The SaveCCM Language Reference Manual.

Uppaal PORT is developed based on source code of the Uppaal model-checker. The analysis is performed on a symbolic representation of the hierarchical component structure of the input model (without transformation to a "flat" system of timed automata).

Uppaal PORT has been developed within the SAVE and SAVE++ projects, and the Progress centre.


Uppaal PORT is distributed under the same license as the Uppaal tool. It is free for non-commercial applications in academia, and for private persons. For commercial applications a commercial license is required.


PORT identifies a point of interaction where required and provided interfaces of a component are specified. Uppaal PORT supports Component-Based Development with analysis of component models (without flattening the model, or translating to a netowork ordinary timed automata) and utilizes the model structure to improve analysis performance.

PORT is an acronym from Partial Order Reduction Techniques, which are implemented in (but currently not available in the distributed version of) the Uppaal PORT tool to improve its runtime performance.


The latest version 0.48 is available for download, see also the release notes.