Introduction
Here are the highlights of Uppaal TRON features:
- Performs conformance testing: the tool checks whether the timed runs of the system under test (SUT) are specified in the system model (timed trace inclusion) and no illegal (unexpected, unspecified) timed behavior is observed.
- The emphasis is on testing the timed and functional properties. Time is considered continuous, (input/output) events can happen at any real-valued moment in time, but deadlines are constrained by integers (rationals). Test data generation is also possible, but (today) data types and value selection are limited by modeling language.
- The specification is an Uppaal timed automata network partitioned into a model of the system and a model of system's environment assumptions. The model can be non-deterministic, allowing reasonable freedom for system implementations, modeling possible/tolerable time drifts, soft time deadlines.
- Test primitives are generated directly from the model, executed and the system responses checked at the same time, online (on-the-fly) while connected to the SUT, thus avoiding huge intermediate test suites.
- During testing the tool follows the environment model
which can have various purposes:
- fully permissive environment model allows to test full conformance;
- a specific environment minimizes the testing effort for realistic level of conformance;
- environment model as use cases guide through functionality of a particular interest;
- environment model as pre-recorded test runs used to re-execute tests for debugging or regression testing.
- Uppaal model-checking engine allows efficient and fast timed automata model exploration.
- The choices of inputs and time delays are randomized.
- In general, testing the real-time conformance is undecidable, but under digitization assumptions it is shown to be sound and complete in a limit.
Uppaal TRON Setup
The system under test is attached to Uppaal TRON via a test-adapter (an SUT specific software layer) and considered as a black-box since its state cannot be directly observed; only communication events via input/output channels. The user supplies Uppaal TRON 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.