Abstract
Model-based test generation consists in deriving system traces from specifications of systems under test. There exist several
techniques for test generation, which, however, may suffer from scalability problems. In this paper, we assume that the system
under test can be divided in several subsystems such that only one subsystem is active at the time. Moreover, each subsystem
decides when and to which other subsystem to pass the control, by also initializing the initial state of the next subsystem
in a desired way. We model these systems and we show how it is possible to generate tests in a very efficient way that exploits
the division of the entire system in subsystems. Test generation for the whole system is performed by visiting each subsystem
and generating tests for it. The tests are combined in order to obtain valid system traces. We show how several visiting policies
influence the completeness of the test generation process.
[read the copyright and download the pdf file] [DOI] [url] [Abstract State Machines, Alloy, B, VDM, and Z Selected and extended papers from \ABZ\ 2012]