Mutation testing

Description of the Case Study

Another application of hyperproperties with quantifier alternation is the efficient generation of test suites for mutation testing. We 22 borrow a model from [FBW19] and apply the original formula that describes a good test mutant together with the model, expressed as:

\[\varphi_{\text{mut}} = \exists \pi_A . \forall \pi_B \left( mut_{\pi_A} \land \neg mut_{\pi_B} \right) \land \left( \left( in_{\pi_A} \leftrightarrow in_{\pi_B} \right) \ \mathcal{U} \ \left( out_{\pi_A} \not\leftrightarrow out_{\pi_B} \right) \right)\]

HyperQB returns SAT which implies the successful finding of a qualified mutant.

Benchmarks

Case #6.1

The Model(s)

Mutation Testing

-- MUTATION TESTING
-- (adopted from: . Andreas Fellner, Mitra Tabaei Befrouei, and Georg Weissenbacher. Mutation testing with hyperproperties. In Proc. of the 17th Int’l Conf. on Software Engineering and Formal Methods (SEFM’19))
MODULE main
VAR
    mutation: boolean;
    action: 0..2;
    beverage: 0..2;
    water: 0..3;


ASSIGN
    init(mutation) := {TRUE, FALSE};
    next(mutation) := {TRUE, FALSE};

    init(action) := 0;
    next(action) := {0,1,2};

    init(beverage) :=0;
    next(beverage) :=
        case
            (action=1 & !(water=0)): 1;
            TRUE: beverage;
        esac;

    init(water) :=2;
    next(water) :=
        case
            (action=1 & !(water=0)): water - 1; -- make beverage
            (mutation & water=0): 1;
            (mutation & water=1): 2;
            (mutation & water=2): 3;
            (mutation & water=3): 3;
            (!mutation & water=0): 2;
            (!mutation & water=1): 3;
            (!mutation & water=2): 3;
            (!mutation & water=3): 3;
            TRUE: water;
        esac;

DEFINE
    NO_water := (action=1) & (water=0);
    NO_output := (action!=1)  | ((action=1)&(beverage=0));

Formula

exists A. forall B. 
((*action[A] = action[B]*) U ( (*beverage[A] = beverage[B]*) \/ (*water[A] = water[B]*) \/ ~(NO_water[A] <-> NO_water[B]) \/ ~(NO_output[A] <-> NO_output[B])))