Welcome to T-Uppaal Homepage

Overview

  1. News
  2. What is T-Uppaal
  3. Status of the Project
  4. Download and Install
  5. Documentation
  6. Talks
  7. Publications
  8. License Agreement
  9. Problems and Bugs
  10. About the Authors

News

February 28, 2005. T-Uppaal from now on is called Uppaal TRON and can be found here. Maintaining is moved there too.

February 7, 2005. T-Uppaal version 1.3.0 is out. Summary of the progress:

In 1.3.0:
* Environment invariants are supported (to the extent of CPU time available).
* Simple observation uncertainty added to time-stampping.
* Data value binding supported in input/output actions.
* New adapter API.

November 30, 2004. T-Uppaal versions 1.1.3 and 1.2 are out. Summary of the progress:

In 1.2:
* the first implementation of smart delay choice.
* no need for zzz hack, invariants on environment are respected.
* the coverage of the model is poor since the algorithm is not
  completely randomized because of smart delay choice (you may want to
  use 1.1.3 version).

In 1.1.3:
* first experiments with observation uncertainty added.
* improved clock synchrony.
* fixed bug in the driver: last delay reporting.
* no smart delay implementation, zzz hack is still needed.

What is T-Uppaal

T-Uppaal is a testing tool for black-box conformance testing of embedded and real-time systems. Given a formal timed automata model of the system under test (SUT) and its assumed operating environment, T-Uppaal automatically generates and executes timed test sequences. T-Uppaal is an online testing tool which means that it continuously executes test events on the SUT as they are being generated, and events from the SUT is checked against the model. The observed behavior is required to be timed trace included in the specification.

The tool is based on the Uppaal engine which is a model-checker of real-time systems modeled as networks of timed automata.

The system under test is attached to T-Uppaal via a test-adapter (an SUT specific software layer) and considered as a black-box since its states cannot be directly observed; only communication events via input/output channels. The user supplies T-Uppaal with the closed timed automata network of SUT model in parallel composition together with assumptions on environment.

The explicit environment model is an important feature: it can be used to generate test events only that are realistic it the operating environment. It may also be fully-permissible, meaning that the environment (testing tool in this case) can offer any input at any moment and accept any output at any moment. Finally it can be used to guide the test (which is randomized) to produce particularly interesting behaviors.

Status of the Project

Now T-Uppaal version 1.2 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 Uppaal 3.4.2. Current availability and limitations:

  1. 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.
  2. Input and output actions through channel handshake synchronization (no buffering or value passing).
  3. User supplied adapter loading via dynamic library interface.
  4. Adapter development framework (C++), interfaces are not completely stabilized yet.
  5. Examples of tool applications against C++ programs as IUT.
  6. No graphical user interface. Use Uppaal to create and edit models.
  7. Stripped binary executable form of T-Uppaal. No source code provided due to licensing restrictions. Binary is dynamically linked in order to provide efficient connectivity with user-supplied adapter.
  8. Tool prepared on the following platforms:
    OSCompilers
    Sun OS 5.9 on SPARC GNU Compiler Collection 3.3.1
    Linux 2.6.5 on intel GNU Compiler Collection 3.3.5 from Debian SID
    It should also work on other kernels and distributions (e.g. Sun OS 5.8 on SPARC or Red Hat Enterprise 3 with Linux-2.4.21), it is important that the machine architecture should match and GCC-2 should not be mixed with GCC-3. Please report your experiences.

Note for RedHat users: RedHat seems to include old libxml2 libraries, where T-UPPAAL-1.3.0 needs at least libxml2-2.6.11. Solution: try to upgrade your system or compile libxml2-2.6.11 for your local settings, you may need to set LD_LIBRARY_PATH to lib directory where libxml2 is installed.

Download

Here is T-Uppaal licence agreement and download page.

You may want to download and try Uppaal to create, edit and verify the test specification before using T-Uppaal.

Documentation

Please see the README file from installation package.

A small guide to T-Uppaal soon to appear...

Talks

  1. Online Testing of Real-time Systems. Marius Mikucionis. Basic Research in Computer Science Seminar Series. Aalborg, Denmark. October 13, 2004. [pdf]
  2. T-UPPAAL: Real-Time Online Testing Tool. Marius Mikucionis, Kim G. Larsen, Brian Nielsen. Presentation for Systematic Testing of Realtime Embedded Software Systems (STRESS) project, Twente University, The Netherlands. February, 2004. [pdf]

Publications

  1. T-UPPAAL: Online Model-based Testing of Real-time Systems. Marius Mikucionis, Kim G. Larsen, Brian Nielsen. 19th IEEE International Conference on Automated Software Engineering, 396-397. Linz, Austria. September 24, 2004. [ps]
  2. Online Testing of Real-time Systems Using UPPAAL. Kim G. Larsen, Marius Mikucionis Brian Nielsen. Formal Approaches to Testing of Software. Linz, Austria. September 21, 2004.
  3. Online On-the-Fly Testing of Real-time Systems. Marius Mikucionis, Kim G. Larsen, Brian Nielsen. Basic Research In Computer Science Report Series. Aalborg, Denmark. December, 2003. ISSN 0909-0878. [bib] [abstract] [pdf]
  4. Real-time System Testing On-the-fly. Marius Mikucionis, Brian Nielsen, Kim G. Larsen. The 15th Nordic Workshop on Programming Theory. Turku, Finland. October 29-31, 2003. [bib] [pdf]
  5. On-the-fly Testing Using UppAal. Marius Mikucionis, Egle Sasnauskaite. Master thesis, Department of Computer Science, Aalborg University. June 11, 2003. [pdf]

License Agreement

Since T-Uppaal is just and extension to Uppaal we must obey the original Uppaal license, and the full extended license is the following:

     

Copyright (c) 1995-2004 by Uppsala University and Aalborg University.

We (the licensee) understand that Uppaal includes the programs: uppaal2k.jar, uppaal, uppaal.bat, server, socketserver, atg2ugi, atg2ta, atg2hs2ta, hs2ta, checkta, simta, verifyta, uppaal, xuppaal, tuppaal, and tuppaal-s 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.

     

Problems and Bugs

Please send your bug-reports (error message and a procedure to replicate the problem) to marius@cs.aau.dk. Note that sometimes it is extremely hard to replicate the problem because of multi-threaded context switching. The current installation bugs and workarounds a available here.

About the Authors

The tool development is carried out in close collaboration with Uppaal team from Uppsala University in Sweden and Aalborg University in Denmark.

Currently the tool implementation is a part of Marius Mikučionis' Ph.D. project "Model-based Testing of Embedded Systems" supervised by Kim G. Larsen and Brian Nielsen. The Ph.D. project is funded by Basic Research in Computer Science at Aalborg University, Denmark.

T-Uppaal development started as a master student project by Eglė Sasnauskaitė-Holgersen, Stanislav Levchenko and Marius Mikučionis as proposed by supervisors Brian Nielsen and Kim G. Larsen in September 2002.


Last updated on Tuesday March 01, 2005 by Marius Mikučionis
Valid XHTML 1.0 Strict