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 |
Optionen (nur für Redakteure)
Redaktionelle Details anzeigen |