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, 23 (6)
doi: 10.1007/s10009-020-00574-z
Artikel, Bibliographie
Dies ist die neueste Version dieses Eintrags.
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 |
| Verlag: | Springer |
| Titel der Zeitschrift, Zeitung oder Schriftenreihe: | International Journal on Software Tools for Technology Transfer |
| Jahrgang/Volume einer Zeitschrift: | 23 |
| (Heft-)Nummer: | 6 |
| DOI: | 10.1007/s10009-020-00574-z |
| Zugehörige Links: | |
| 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 |
| Zusätzliche Informationen: | Erstveröffentlichung; Special Issue: TestComp 2019 |
| 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: | 08 Mai 2024 11:41 |
| PPN: | |
| Export: | |
| Suche nach Titel in: | TUfind oder in Google |
Verfügbare Versionen dieses Eintrags
-
CPA/Tiger-MGP: test-goal set partitioning for efficient multi-goal test-suite generation. (deposited 30 Apr 2024 11:27)
- CPA/Tiger-MGP: test-goal set partitioning for efficient multi-goal test-suite generation. (deposited 15 Jun 2020 07:47) [Gegenwärtig angezeigt]
 |
Frage zum Eintrag |
Optionen (nur für Redakteure)
 |
Redaktionelle Details anzeigen |
Drucken
Impressum