BZ-TT: A tool-set for test generations from Z and B using constraint logic programming

In this paper, we present an environment for boundary-value test generation from Z and B specifications. The test generation method is original and was designed on the basis of several industrial case-studies in the domain of critical software (Smart Card and transport areas). It is fully supported by a tool-set: the BZ-Testing-Tools environment. The method and tools are based on a novel, set-oriented, constraint logic programming technology. This paper focusses on how this technology is used within the BZ-TT environment, how Z and B specifications are translated into constraints, and how the constraint solver is used to calculate boundary values and to search for sequences of operations during test generation