Formal Analysis of Reachability, Infection and Propagation Conditions in Mutation Testing

TL;DR

This paper introduces a formal method using weakest precondition calculus to accurately determine reachability, infection, and propagation conditions in mutation testing, enhancing test case generation for killing mutants.

Contribution

It presents a novel formal approach employing weakest precondition calculus and a new reachability function to analyze RIP conditions in mutation testing.

Findings

Method successfully applied to four example programs

Accurately calculates RIP conditions for mutants

Demonstrates applicability through case studies

Abstract

Finding test cases to kill the alive mutants in Mutation testing needs to calculate the Reachability, Infection and Propagation(RIP) conditions and full test specification. In this paper, a formal approach to calculate RIP conditions is proposed. The Dijkestra's weakest precondition predicate transformer (wp(_,_)) is used to calculate infection and propagation conditions. The rc(_) function is defined to calculate the reachability conditions generated by each statement. Four programs and their mutants are examined as running examples and as case studies to show the applicability of the method.