trap properties

A trap property is the negation of the original (desired) property for systems. It plays important notion in a techniques of test-cases generation using model checking.

The techniques of test-cases generation using model checking consists of four steps. First, the design models are mapped to finite state automata suitable for model checkers.
Second, the test criteria (test purpose) are encoded into temporal logic, such as CTL or LTL formulae.
Third, a counterexample is generated if the model does not satisfy the temporal logic formula. A counterexample is an execution trace that will take the finite state model from its initial state to a state where the violation occurs.

Finally, a test case can be retrieved from the counterexample. To achieve test coverage, the test criterion will be encoded into a set of trap properties, so that test cases satisfying the test criterion can be retrieved from a set of counterexamples.

cite:

International Conference on Information Technology (ITNG'07)
A Model Checking based Test Case Generation Framework forWeb Services (PDF)
Las Vegas, Nevada, USA
April 02-April 04
ISBN: 0-7695-2776-0
Yongyan Zheng, University of Surrey
Jiong Zhou, University of Surrey
Paul Krause, University of Surrey