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.
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.
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:
| OS | Compilers |
|---|---|
| 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 |
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.
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.
Please see the README file from installation package.
A small guide to T-Uppaal soon to appear...
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:
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. |
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.
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 by Marius Mikučionis |
|