Premium
A new method for testing timed systems
Author(s) -
Bonifácio Adilson Luiz,
Moura Arnaldo Vieira
Publication year - 2013
Publication title -
software testing, verification and reliability
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.216
H-Index - 49
eISSN - 1099-1689
pISSN - 0960-0833
DOI - 10.1002/stvr.454
Subject(s) - computer science , correctness , automaton , granularity , flexibility (engineering) , grid , formal specification , programming language , implementation , theoretical computer science , mathematics , statistics , geometry
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.