Figure: Uppaal PORT in SAVE IDE on screen.
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 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.