Automated Generation of Test Cases from Contract-Oriented Specifications: A CSP-Based Approach

In this paper, we discuss the automated generation of test cases from contract-oriented specifications. The static analysis we develop rely on original constraint minimization and satisfaction techniques (CSP). We propose a flexible CSP architecture that can apply not only on integer or bounded domains but also on arbitrary types. The original notion of type builders is used to establish the connection between the type semantics and the CSP framework. We illustrate this aspect by developing a string builder that can automatically generate string instances depending on combinations of constraints based on string sizes and substrings. The scope of these techniques goes beyond the generation of test cases. They are used in other static analyzes, most notably a symbolic animation of contracts that can detect inconsistencies early in the development cycle.