Fault-based testing is a technique where testers anticipate errors in a system under test in order to assess or generate test cases. The idea is to have enough test cases capable of detecting these anticipated errors. This work presents a method of fault-based test case generation for pre- and postcondition specifications. Here, errors are anticipated on the specification level by mutating the pre- and postconditions. We present the underlying theory by giving test cases a formal semantics and translate this general testing theory to a constraint satisfaction problem. A prototype test case generator serves to demonstrate the automatization of the method. It works on OCL specifications.
