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.
2014
Arcaini, Paolo; Gargantini, Angelo Michele; Riccobene, Elvinia
File allegato/i alla scheda:
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

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/10446/30876
Citazioni
  • Scopus 5
  • ???jsp.display-item.citation.isi??? ND
social impact