TRON2UPPAAL Backtracer Tool – From TRON Logs to UPPAAL Traces

UPPAAL TRON is a tool for on-line black-box conformance testing of real-time systems. Typically, the model-based specifications are edited, simulated, and verified in the UPPAAL model-checker and, later on, used in UPPAAL TRON for testing the Implementation Under Test (IUT). Whenever a non-conformance is detected between the specifications and IUT, a failed or inconclusive verdict is given. Analysing the test logs in order to identify the path taken in the specification and the source of the failure is tedious and time consuming, especially for long lasting test sessions. Therefore, in order to reduce the time and effort for debugging test sessions, we propose a tool-supported approach to transform TRON logs into a UPPAAL simulation trace. This allows us to take advantage of UPPAAL’s capabilities for simulation and visualisation of the test traces. The approach is exemplified and evaluated on a traditional Smart Light controller example provided by UPPAAL TRON. The results show that the approach is scalable enough to be applied to more complex examples.

Junaid Iqbal, Dragos Truscan, Jüri Vain, Ivan Porres (Åbo Akademi University): TRON2UPPAAL Backtracer Tool – From TRON Logs to UPPAAL Traces. TUCS Technical Reports 1138, Turku Centre for Computer Science, 2015.