Preamble computation in automated test case generation using constraint logic programming

摘要

BZ-Testing-Tools (BZ-TT) is a tool-set for automated model-based test case generation from B machines and Z specifications. BZ-TT uses boundary testing as well as cause-effect testing on the basis of the formal model. It has been used and validated on several industrial case studies in the domain of critical software: in particular for smart card applications and automotive embedded systems. The main idea of BZ-TT is to compute a boundary goal for each effect of the operations of the model and then to compute a preamble sequence of operations to place the system under test in such a state that satisfies the goal. In this paper, the preamble computation search strategies used in BZ-TT are presented. More precisely, two algorithms based respectively on forward chaining and backward chaining are compared. These algorithms both use a customized set constraint solver, which is able to animate the formal model. These algorithms differ, however, in their capacity to reach the boundary goals efficiently. The results of applying the tools to an industrial windscreen wiper controller application are presented.