Home

Welcome to the Testing_with_TRON wiki!

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.).

Uppaal TRON is a testing tool, based on Uppaal engine, suited for black-box conformance testing of timed systems, mainly targeted for embedded software commonly found in various controllers. By online we mean that tests are derived, executed and checked simultaneously while maintaining the connection to the system in real-time.

A simplest closed system suitable for testing using TRON consists of at least two communicating processes: IUT process and environment process. In this simple system, the input event is fired whenever environment process shouts at some channel and IUT receives the channel synchronization, the output happens in the same manner but opposite direction.

It is important that environment is input enabled, i.e. it is able to consume any possible output produced by IUT, otherwise, TRON will issue verdict "inconclusive" in case the received output event cannot be applied to the environment.

In a more complex system, the IUT (and environment) requirements may be modeled by many processes. In this case, the system is partitioned into two sets of processes: the processes modelling the requirements for IUT (model of IUT) typically mimicking what the IUT should do and the processes for the environment assumptions (model of the environment) mimicking what the tester should do. The IUT (environment) processes may communicate among themselves by channel synchronizations too, but such communication is treated as internal and not observable. The channel synchronization is treated as observable input/output event if and only if it is between the environment and IUT processes.

Regarding the channel synchronization is an instantaneous event in timed automata network, hence the communication between the environment and the IUT is also treated as instantaneous. However real-time black-box testing is also a kind of remote testing, where the inputs/outputs are fed at one-time instance and received slightly later as there is at least small communication delay. Even the slightest delay of electronic signal running a short distance at a speed of light is significant as it might imply a different input and output event interleaving and hence a different outcome. The communication delay is especially significant on soft-real-time operating systems (such as Windows and Linux) where the process scheduling is a major contributor but is hardly predictable (Linux scheduler tries hard to be at most 10ms late and 2.6 branch usually fits into 1ms delay under low load conditions, see Latency Experiments). Currently, TRON time-stamps the input and output events when they arrive/leave TRON process, hence the model of IUT should also include the processes of adapter proxying and slightly delaying the actual input and output to reflect such communication reality. The model of adapter also helps to make sure that the model of IUT is input enabled, i.e. IUT cannot refuse to accept the offered input, which might be important in testing features that are triggered only by that particular input (and time). TRON will not try to offer an input if the model of IUT is not able to consume it.

To understand the multiview modeling

1. Vain, Jüri; Kaur, Apneet; Tsiopoulos, Leonidas; Raik, Jaan; Jenihhin, Maksim (2017). Modeling for multi-view interference analysis of design aspects in MPSoC designs. Proceedings of 22nd IEEE European Test Symposium : RESCUE 2017, Workshop on Reliability, Security and Quality, May 25-26, 2017, Limassol, Cyprus. KIOS Research Center | University of Cyprus, 1−6

To understand the Multi-fragment Markov model guided online test generation for MPSoC

2. Vain, Jüri; Tsiopoulos, Leonidas; Kharchenko, Vyacheslav; Kaur, Apneet; Jenihhin, Maksim; Raik, Jaan (2017). Multi-fragment Markov model guided online test generation for MPSoC. ICT in Education, Research and Industrial Applications : Integration, Harmonization and Knowledge Transfer : Proceedings of the 13th International Conference, ICTERI 2017, Kyiv, Ukraine, May, 2017. Ed. Ermolayev, V. et al. Aachen: RWTH Aachen University, 594−607. (CEUR Workshop Proceedings; 1844).