Mutation Testing (NuSMV)

Description of the Case Study

Another application of hyperproperties with quantifier alternation is the efficient generation of test suites for mutation testing. We 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

The Model(s)

-- 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;

    NO_water: boolean;
    NO_output: boolean;


ASSIGN
    init(NO_water) := FALSE;
    next(NO_water) :=
    case
        ((action = 1) & (water = 0)): TRUE;
        TRUE: NO_water;
    esac;


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


    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])))

References