Test Model Coverage Analysis under Uncertainty

TL;DR

This paper introduces an extension to probabilistic model checking that enables efficient calculation of aggregate coverage metrics, including k-wise coverage, for non-deterministic models in model-based testing.

Contribution

It presents a novel method for computing probabilistic aggregate coverage and k-wise coverage in non-deterministic models, addressing limitations of existing analysis techniques.

Findings

Efficient calculation of probabilistic aggregate coverage achieved.

Extension supports k-wise coverage analysis.

Applicable to models with estimated transition probabilities.

Abstract

In model-based testing (MBT) we may have to deal with a non-deterministic model, e.g. because abstraction was applied, or because the software under test itself is non-deterministic. The same test case may then trigger multiple possible execution paths, depending on some internal decisions made by the software. Consequently, performing precise test analyses, e.g. to calculate the test coverage, are not possible. This can be mitigated if developers can annotate the model with estimated probabilities for taking each transition. A probabilistic model checking algorithm can subsequently be used to do simple probabilistic coverage analysis. However, in practice developers often want to know what the achieved aggregate coverage, which unfortunately cannot be re-expressed as a standard model checking problem. This paper presents an extension to allow efficient calculation of probabilistic aggregate coverage, and moreover also in combination with k-wise coverage.