Positive and Negative Testing with Mutation-DrivenModel Checking
Zhenyu Chen · 2012
Abstract: Mutation-driven test case generation with model checking has been proposed to reduce the costs of specification-based mutation analysis. Most of the existing work focuses on verifying the expected behavior in the original model, i.e. positive testing. In this paper negative testing is introduced to check the unexpected behavior. Mutants are divided into three types: increscent, decrescent, and cross mutants. Both, positive and negative testing is proposed to guarantee the detection of these mutants. Anon-trivial example illustrates and validates our approach. 1 Introduction and Related Work Mutation analysis is acommonly accepted technique of fault-based testing that considers faults that cause small changes to the system under test [1, 2]. Mutation analysis has been primarily used for code-based testing techniques, butithas been extended to specificationbased testing in recent years. In this context, model checking can be used to compare the