tap2014 Paolo Arcaini Angelo Gargantini Elvinia Riccobene

An Abstraction Technique for Testing Decomposable Systems by Model Checking

in 8th International Conference on Tests & Proofs, July 24 - July 25, 2014, York, UK (Eds. Seidl, Martina and Tillmann, Nikolai) Springer International Publishing, Lecture Notes in Computer Science, vol. 8570 (2014): 36-52

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]