A new method for testing timed systems. (9th March 2011) - Bonifácio, Adilson Luiz; Moura, Arnaldo Vieira
SUMMARY Devising formal techniques and methods that can automatically generate test suites for timed systems has remained a challenge. In this paper Timed Input/Output Automata (TIOA) are used as a formal specification model for timed systems. This work proposes and proves the correctness of a new and more general discretization method that can be used to obtain grid automata corresponding to specification TIOA, using almost any granularity of interest. Such flexibility to find a suitable granularity opens the possibility for a more compact construction of grid automata. It is also shown how test purposes can be used together with the specification TIOA in order to generate grid automata that capture the behavior of both the specification and the test purpose. From such grid automata one can algorithmically extract test suites that can be used to verify whether given implementations adhere to the specification and reflect the properties modeled using the test purposes. Copyright © 2011 John Wiley & Sons, Ltd.