Theta: Modular Model Checker Built For Diverse Algorithm Configurations (Accompanying Artifact)

Accompanying artifact for our paper entitled "Theta: Modular Model Checker Built For Diverse Algorithm Configurations".

We used Theta version 6.12.2, available under v6.12.2.

README: Theta Benchmarking Artifact

Overview

This Zenodo artifact accompanies our paper on benchmarking Theta, a model checker framework. The artifact includes all necessary files for reproducing our benchmarking experiments and analyzing the results.

We retracted the following XSTS models from the archive due to their confidential nature:

- INPE: A composite system modeling two components a communication protocolinside a nanosatellite, provided by the brazilian National Institute for SpaceResearch (see http://www.inpe.br).

- COID and PIL: Gamma statechart networks modeling components of railway safetyequipment. Provided by a confidential partner from the railway industry.

Artifact Structure

The artifact consists of the following directories and files:

binary/: Contains Theta's JAR files, solvers, and required shared libraries.

benchmarks/: Includes all benchmarks used in the evaluation, with expected verdicts where known.

benchexec/: Contains the version of BenchExec used for the experiments.

results/: Stores the benchmarking results.

tooldefs/: Holds BenchExec tool definitions for Theta (slightly modified from the official tool info module).

variants.csv: Lists all configurations used in the experiments.

create-variants.py: Generates benchmark definition files (pre-generated in this artifact).

get-latest-files.sh: Helper script to retrieve the latest result files.

get-portfolios.py: Script to generate quantile plots.

get-results.py: Script to parse results and generate the summary table.

run-all.sh: Main script to execute all benchmark runs.

run-benchmark.sh: Script to execute a specific benchmark configuration.

svcomp.def: Benchmark definition file.

Reproducing Results

To reproduce the results, follow these steps:

Modify run-benchmark.sh (if necessary) to use a non-Slurm-based BenchExec setup.

Navigate to the binary/ folder and execute:

source ../run-all.sh

This will re-run all experiments that do not have a corresponding folder in results/. To fully reproduce the results, delete the results of specific configurations before rerunning.

Analyzing Results

To generate the results table, run:

python get-results.py

To generate the quantile plot, run:

get-latest-files.sh | python get-portfolios.py

Threats to Validity

The following factors may threaten the validity of this experiment: 

Internal Validity.

Reliability of the experiments were ensured by using the BenchExec framework. The number of solved tasks may be influenced by environmental effects, therefore, small differences are disregarded.

External Validity.

The generalizability of the experimental results may be limited by the relatively small number of benchmarks used. 

 Construct Validity.

Academic competitions like SV-COMP showcase the performance of tools after extensive tuning and repeated testing on a fixed benchmark set. As a result, our findings may not be easily reproducible on a different, less used set of benchmarks.