Figure 1: Uppaal on screen.
Uppaal is an integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata, extended with data types (bounded integers, arrays, etc.).
News: The current official release is Uppaal 4.0.13 (Sep 27, 2010). Compared to version 3, the 4.0 release is the result of over 2.5 years of additional development, and many new features and improvements are introduced (see also this release note and the web help section new features). To support models created in previous versions of Uppaal, version 4.0 can convert most old models directly from the GUI (alternatively it can be run in 3.4 compatibility mode by defining the environment variable UPPAAL_OLD_SYNTAX, see also item 2 of the FAQ).
Since Feb 26 2008, we also distribute a development snapshot of the forthcoming Uppaal 4.2. The current development snapshot version is 4.1.15 released April 19th, 2013.
The Uppaal tool is free for non-commercial applications in academia only. For commercial applications a commercial license is required. Please see the Download section or www.uppaal.com for more information.
Uppaal has an open discussion forum group at Yahoo!Groups intended for users of the tool. To join or post to the forum, please refer to the information at the discussion forum page. Bugs should be reported using the bug tracking system. To email the development team directly, please use uppaal(at)list(dot)it(dot)uu(dot)se.
In our ongoing work to localize the Uppaal GUI we would like to acknowledge contributions by the following external people:
- Hiroshi Fujimoto (JA)
- Line Juhl (DK)
- Shuhao Li (ZH)
- Marius Mikucionis (LT)