Abstract
Test generation by model checking exploits the capability of model checkers to return counterexamples upon property violations.
The approach suffers from the \emphstate explosion problem of model checking. For property verification, different abstraction
techniques have been proposed to tackle this problem. However, such techniques are not always suitable for test generation.
In this paper we focus on Decomposable by Dependency Asynchronous Parallel (DDAP) systems, composed by several subsystems
running in parallel and connected together in a way that the inputs of one subsystem are provided by another subsystem. We
propose a test generation approach for DDAP systems based on a decompositional abstraction that considers one subsystem at
a time. It builds tests for the single subsystems and combines them later in order to obtain a global system test. Such approach
avoids the exponential increase of the test generation time and memory consumption. The approach is proved to be sound, but
not complete.
[ read the copyright and download the pdf file] [ DOI] [ url] [ presentation]