Test generation by model checking exploits the capability of model checkers to return counterexamples upon property violations. The approach suffers from the \emph{state 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.
(2014). An abstraction technique for testing decomposable systems by model checking [conference presentation - intervento a convegno]. Retrieved from http://hdl.handle.net/10446/30876
An abstraction technique for testing decomposable systems by model checking
ARCAINI, Paolo;GARGANTINI, Angelo Michele;
2014-01-01
Abstract
Test generation by model checking exploits the capability of model checkers to return counterexamples upon property violations. The approach suffers from the \emph{state 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.File | Dimensione del file | Formato | |
---|---|---|---|
decompAbstractTap2014_cameraReady.pdf
Solo gestori di archivio
Descrizione: author's postprint - versione referata
Dimensione del file
487.29 kB
Formato
Adobe PDF
|
487.29 kB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
Aisberg ©2008 Servizi bibliotecari, Università degli studi di Bergamo | Terms of use/Condizioni di utilizzo