Test generation by model checking exploits the capability of model checkers to return counterexamples upon property violations. The approach suffers from the 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.

An abstraction technique for testing decomposable systems by model checking / P. Arcaini, A. Gargantini, E. Riccobene (LECTURE NOTES IN COMPUTER SCIENCE). - In: Tests and Proofs : 8. International conference, TAP 2014, held as part of STAF 2014 : York, UK, July 24–25, 2014 : proceedings / [a cura di] M. Seidl, N. Tillmann. - Prima edizione. - Switzerland : Springer, 2014. - ISBN 9783319090986. - pp. 36-52 (( Intervento presentato al 8. convegno International Conference on Tests and Proofs tenutosi a York (UK) nel 2014 [10.1007/978-3-319-09099-3_3].

An abstraction technique for testing decomposable systems by model checking

E. Riccobene
2014

Abstract

Test generation by model checking exploits the capability of model checkers to return counterexamples upon property violations. The approach suffers from the 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.
computer science (all); theoretical computer science
Settore INF/01 - Informatica
Book Part (author)
File in questo prodotto:
File Dimensione Formato  
chp%3A10.1007%2F978-3-319-09099-3_3.pdf

accesso riservato

Tipologia: Publisher's version/PDF
Dimensione 459.67 kB
Formato Adobe PDF
459.67 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

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