CPA/Tiger-MGP: Test-Goal Set Partitioning forEfficient Multi-Goal Test-Suite Generation – Replication Package

Abstract

Software model checkers can generate high-quality test cases from counterexamples of a reachability analysis. However, naively invoking a 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 model checker for all test goals in a single run leads to low abstraction possibilities and thus to low scalability. Our approach therefore pursues a test-suite generation technique that allows for configurable multi-goal set partitioning (MGP), using configurable partitioning strategies, and simultaneous processing of multiple test goals in one reachability analysis. Our approach therefore 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 frameworkCPAchecker.

Supplementary Data

Artifact Download
CPA/Tiger-MGP 1, 2, 3
Benchmark definition XML
Results Test-Comp

 

Reproducing the Results

The submitted Version of CPA/Tiger-MGP for Test-Comp is built from revision 30601 from the official CPAchecker repository, branch tigerIntegration2.

To run CPA/Tiger-MGP, enter the following command:

  • scripts/cpa.sh -benchmark -heap 10000M -tigertestcomp19 -spec spec.prp task

where spec is either coverage-error-call or coverage-branches and task is the c or intermediate file to be analysed. CPA/Tiger-MGP prints statistics of the run to the console and writes test-cases and test-suite meta-data in the output folder. To reproduce the results, use a Linux system with Java 8 runtime environment, BenchExec, SV-Benchmarks and run Benchexec with the following files:

  • the benchmark definition cpa-tiger.py which is archived at gitlab. com/sosy-lab/test-comp/bench-defs/tree/master/benchmark-defs
  • the tool-info module cpachecker.py which can be found at github. com/sosy-lab/benchexec/tree/master/benchexec/tools

Kontakt

Technische Universität Darmstadt

Fachbereich Elektrotechnik und Informationstechnik

Fachgebiet Echtzeitsysteme

Prof. Dr. rer. nat. Andy Schürr

Magdalenenstr. 4

64289 Darmstadt

+49(0)6151 16-22350

+49(0)6151 16-22352

Drucken | Impressum | Datenschutzerklärung | Sitemap | Suche | Kontakt
Zum SeitenanfangZum Seitenanfang