Require, Test and Trace IT

B. K. Aichernig, F. Lorber, D. Nickovic, and S. Tiran

Abstract:

We present a framework for requirement-driven test-case generation from specifications of synchronous reactive systems. We propose requirement interfaces as the formal specification model. Contract specifications of individual requirements are naturally combined by the conjunction operation. The conjunction of two requirement interfaces has the property that it subsumes all behaviors of the individual interfaces. We exploit this property to generate test cases incrementally. We use a small set of related requirements to drive test-case generation, thus avoiding the explosion of the state space to explore. In addition to test-case generation, we also provide a procedure for incremental consistency checking of the requirements. Our requirement-driven approach has several advantages: (1) both consistency checking and test case generation are incremental and thus more efficient; (2) test cases are naturally related to requirements, hence enabling easier traceability; and (3) fail verdicts in a test case can be mapped to violated requirements. We implemented a prototype using the SMT-solver Z3.

Reference: B. K. Aichernig, F. Lorber, D. Nickovic, and S. Tiran. Require, test and trace it. Technical report, Institute for Software Technology (IST), Graz University of Technology, 2014.