TU Darmstadt / ULB / TUbiblio

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

Ruland, Sebastian ; Lochau, Malte ; Fehse, Oliver ; 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
doi: 10.1007/s10009-020-00574-z
Artikel, Bibliographie

Kurzbeschreibung (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.

Typ des Eintrags: Artikel
Erschienen: 2020
Autor(en): Ruland, Sebastian ; Lochau, Malte ; Fehse, Oliver ; Schürr, Andy
Art des Eintrags: Bibliographie
Titel: CPA/Tiger-MGP: test-goal set partitioning for efficient multi-goal test-suite generation
Sprache: Englisch
Publikationsjahr: 3 Juni 2020
Titel der Zeitschrift, Zeitung oder Schriftenreihe: International Journal on Software Tools for Technology Transfer
DOI: 10.1007/s10009-020-00574-z
URL / URN: https://doi.org/10.1007/s10009-020-00574-z
Kurzbeschreibung (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.

Freie Schlagworte: CPAchecker, Test-goal partitioning, Multi-goal test coverage
Fachbereich(e)/-gebiet(e): 18 Fachbereich Elektrotechnik und Informationstechnik
18 Fachbereich Elektrotechnik und Informationstechnik > Institut für Datentechnik > Echtzeitsysteme
18 Fachbereich Elektrotechnik und Informationstechnik > Institut für Datentechnik
Hinterlegungsdatum: 15 Jun 2020 07:47
Letzte Änderung: 15 Jun 2020 07:47
PPN:
Export:
Suche nach Titel in: TUfind oder in Google
Frage zum Eintrag Frage zum Eintrag

Optionen (nur für Redakteure)
Redaktionelle Details anzeigen Redaktionelle Details anzeigen