Skip to main content.

This page’s menu:

License

Please read the license agreement carefully. The text of the agreement follows:

We (the licensee) understand that UPPAAL includes but is not limited to the programs: uppaal2k.jar, uppaal2k, server, socketserver, atg2ugi, atg2ta, atg2hs2ta, hs2ta, checkta, simta, verifyta, tron, tron-s, uppaal, and xuppaal and that they are supplied "as is", without expressed or implied warranty. We agree on the following:

  1. You (the licensers) do not have any obligation to provide any maintenance or consulting help with respect to UPPAAL.
  2. You neither have any responsibility for the correctness of systems verified using UPPAAL, nor for the correctness of UPPAAL itself.
  3. We will never distribute or modify any part of the UPPAAL code (i.e. the source code and the object code) without a written permission of Wang Yi (Uppsala University) or Kim G Larsen (Aalborg University).
  4. We will only use UPPAAL for non-profit research purposes. This implies that neither UPPAAL nor any part of its code should be used or modified for any commercial software product.

In the event that you should release new versions of UPPAAL to us, we agree that they will also fall under all of these terms.

Requirements

TRON requires Unix environment and GNU C++ compiler (g++) or Microsoft Visual Studio or Sun Java 1.5 for creating custom adapters. It has been built on Debian GNU/Linux SID (unstable) and also for Windows in Cygwin environment using g++ from MingGW so it's very likely to work with C-library adapters built there. There's a small example C-library adapter built by Microsoft compiler, however currently it is only useful to connect to real IUTs in real-time, the virtual-time framework won't work in Windows, unless through TCP/IP socket adapter. Here is the dependency list with Debian package names in parenthesis:

Install them all on Debian:

apt-get install g++ libstdc++6 graphviz r-base gv

Download

By downloading any version of Uppaal, you agree to the above licensing terms.

Please also check the Requirements section.

You may want to read an early draft of user-manual (still under development, comments are welcome).

Status of the Project

Now Uppaal TRON version 1.4 Beta 1 is available. The tool is still in early development and experimental phase, but now anyone can checkout and taste the early fruits on his/her own. The current version is based on the latest Uppaal 4.1. Current availability and limitations:

  1. System specification accepted in Uppaal xta and xml format. The interface is specified separately in adapter library code.
  2. Supported main Uppaal features: clocks, data variables, paired channel synchronizations, urgent locations. The use of arrays, broadcast channel, and committed locations are experimental and not tested.
  3. Input and output actions through channel handshake synchronization (no buffering or value passing).
  4. User supplied adapter loading via dynamic library interface.
  5. Adapter development framework (C++), interfaces are not completely stabilized yet.
  6. Examples of tool applications against C++ programs as IUT.
  7. Use Uppaal to create and edit models.
  8. TRON Tracer GUI demonstrates the main concepts: system model partitioning, interactive traces in testing, system emulation and monitoring.
  9. Graphical user interface is mounted on generic trace-interpreter-adapter (special IUT adapter library) and serves as generic example of how to connect/link to TRON.
  10. Stripped binary executable form of Uppaal TRON. No source code provided due to licensing restrictions. Binary is dynamically linked in order to provide efficient connectivity with user-supplied adapter.
  11. The tool is prepared on the following platforms:
    • Windows 2000 Professional, GNU Compiler Collection 3.4.5
    • Linux 2.6.18 on Intel PC, GNU Compiler Collection 4.1.2
    Latest builds for Sun Solaris could also be provided upon request. It is important that the machine architecture should match and GCC-2 should not be mixed with GCC-3. The same holds for GCC-4. Please report your experiences.

Version History