Abstract
In this paper we describe an approach to use formal analysis tools in conjunction with traditional testing to improve the
efficiency of the test generation process. We have developed a technique for the construction of combinatorial test suites,
featuring expressive constraints over the models under test and cross coverage evaluation between multiple coverage criteria:
combinatorial, structural and fault based. Our approach is tightly integrated with formal logic, since it uses formal logic
to specify the system inputs (including the constraints), test predicates to formalize testing as a logic problem, and applies
the SAL model checker tool to solve it, and hence to generate combinatorial test suites. Early results of experimental assessment
are presented, supported by a prototype tool implementation.