Preamble computation in automated test case generation using constraint logic programming

TLDR

BZ‑Testing‑Tools (BZ‑TT) is a model‑based test case generation tool that uses boundary and cause–effect testing on B abstract machines and Z specifications, computing a preamble sequence to bring the system into a state satisfying each operation’s boundary goal. This paper presents the preamble computation search strategies employed in BZ‑TT. The study compares two algorithms—one using forward chaining and the other backward chaining—both leveraging a customized set‑constraint solver to animate the formal model, differing in their efficiency at reaching boundary goals. The tools have been validated on multiple industrial case studies, including smart card and automotive embedded systems, and the paper reports results from a windscreen wiper controller application. © 2004 John Wiley & Sons, Ltd.

Abstract

BZ-Testing-Tools (BZ-TT) is a tool-set for automated model-based test case generation from B abstract 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. Copyright © 2004 John Wiley & Sons, Ltd.