Test Model Coverage Analysis under Uncertainty
This work addresses a practical challenge for software developers in testing non-deterministic systems, offering an incremental improvement over existing probabilistic model checking methods.
The paper tackles the problem of calculating aggregate test coverage in model-based testing under uncertainty, where non-deterministic models prevent precise analysis, by presenting an extension that efficiently computes probabilistic aggregate coverage, including k-wise coverage.
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.