State Space Coverage Analyses
ProB provides various ways to analyse the coverage of the state space of a model
Event Coverage
[TO DO]
MC/DC Coverage
MC/DC (Modified Condition/Decision Coverage) is a coverage criterion which is used in avionics. One core idea is ensure that for every condition in our code or model we generate at least one test where the condition independently plays an observable role in the outcome of a decision. In other words, if the condition were to be true rather than false (or vice versa) the decision would be changed. In still other words, we are trying to find an execution context where the result of the particular condition under test is crucial for the observable outcome.
In the context of B and Event-B, one question is what constitutes a condition and what constitutes a decision. In WP4 we view a condition to be an atomic predicate (e.g., x>y) not involving logical connectives (&, or, not, =>, ⇔). There is, however, the possibility of treating a bigger predicate as atomic (e.g., an entire guard of an event). The reason for this is to provide better feedback to the user and to reduce the number of coverage criteria if desired. At the moment, we also consider a universally or existentially quantified formula to be a condition. A decision constitutes the fact whether an event is enabled or not. However, we also enable MC/DC to be applied in other contexts, e.g., to analyse invariants; in that setting a decision is whether an invariant is true or false.
We have implemented a MC/DC coverage analysis which examines all visited states and computes the MC/DC coverage for a series of predicates under consideration. Currently MC/DC coverage is used in two ways:
- for the coverage for the invariants, where the invariant is expected to be true (i.e., the analysis does not expect to find states where the invariant is false)
- for the coverage for the event guards. Here it is expected that every event can be enabled or disabled.
The algorithm is parametrised by an optional depth bound: if the depth bound is reached, then all sub-predicates are considered to be atomic decisions. The analysis can be used to measure the coverage of tests, but can also be used after an exhaustive model check to detect vacuous guards and vacuous invariants.
The MC/DC analysis has been integrated into ProB and has been successfully applied to various case studies. Below is a screenshot of part of the output for an early version of the ABZ landing gear case study. It shows that parts of the invariant inv13 not(C0step = 0 & (gearstate = retracting & doorstate /= locked_open & handle = UP)) cannot be set independently to false. This highlights a redundancy in the invariant; indeed the simpler to understand (but stronger) invariant not(gearstate = retracting & doorstate /= locked_open) holds.
