TU Darmstadt / ULB / TUbiblio

CPA/Tiger-MGP: test-goal set partitioning for efficient multi-goal test-suite generation

Ruland, Sebastian and Lochau, Malte and Fehse, Oliver and Schürr, Andy (2020):
CPA/Tiger-MGP: test-goal set partitioning for efficient multi-goal test-suite generation.
In: International Journal on Software Tools for Technology Transfer, ISSN 1433-2787,
DOI: 10.1007/s10009-020-00574-z,
[Article]

Abstract

Software model checkers can be used to generate high-quality test cases from counterexamples of a reachability analysis. However, naïvely invoking a software model checker for each test goal in isolation does not scale to large programs as a repeated construction of an abstract program model is expensive. In contrast, invoking a software model checker for reaching all test goals in a single run leads to few abstraction possibilities and thus to low scalability. Therefore, our approach pursues a test-suite generation technique that incorporates configurable multi-goal set partitioning (MGP) including configurable partitioning strategies and simultaneous processing of multiple test goals in one reachability analysis. Our approach employs recent techniques from multi-property verification in order to control the computational overhead for tracking multi-goal reachability information. Our tool, called CPA/Tiger-MGP, uses predicate-abstraction-based program analysis in the model-checking framework CPAchecker.

Item Type: Article
Erschienen: 2020
Creators: Ruland, Sebastian and Lochau, Malte and Fehse, Oliver and Schürr, Andy
Title: CPA/Tiger-MGP: test-goal set partitioning for efficient multi-goal test-suite generation
Language: English
Abstract:

Software model checkers can be used to generate high-quality test cases from counterexamples of a reachability analysis. However, naïvely invoking a software model checker for each test goal in isolation does not scale to large programs as a repeated construction of an abstract program model is expensive. In contrast, invoking a software model checker for reaching all test goals in a single run leads to few abstraction possibilities and thus to low scalability. Therefore, our approach pursues a test-suite generation technique that incorporates configurable multi-goal set partitioning (MGP) including configurable partitioning strategies and simultaneous processing of multiple test goals in one reachability analysis. Our approach employs recent techniques from multi-property verification in order to control the computational overhead for tracking multi-goal reachability information. Our tool, called CPA/Tiger-MGP, uses predicate-abstraction-based program analysis in the model-checking framework CPAchecker.

Journal or Publication Title: International Journal on Software Tools for Technology Transfer
Uncontrolled Keywords: CPAchecker, Test-goal partitioning, Multi-goal test coverage
Divisions: 18 Department of Electrical Engineering and Information Technology
18 Department of Electrical Engineering and Information Technology > Institute of Computer Engineering > Real-Time Systems
18 Department of Electrical Engineering and Information Technology > Institute of Computer Engineering
Date Deposited: 15 Jun 2020 07:47
DOI: 10.1007/s10009-020-00574-z
Official URL: https://doi.org/10.1007/s10009-020-00574-z
Export:
Suche nach Titel in: TUfind oder in Google
Send an inquiry Send an inquiry

Options (only for editors)
Show editorial Details Show editorial Details