Boundary coverage criteria for test generation from formal models

This paper proposes a new family of model-based coverage criteria, based on formalizing boundary-value testing heuristics. The new criteria form a hierarchy of data-oriented coverage criteria, and can be applied to any formal notation that uses variables and values. They can be used either to measure the coverage of an existing test set, or to generate tests from a formal model. We give algorithms that can be used to generate tests that satisfy the criteria. These algorithms and criteria have been incorporated into the BZ-TESTING-TOOLS (BZ-TT) tool-set for automated test case generation from B, Z and UML/OCL specifications, and have been used and validated on several industrial applications in the domain of critical software, particularly smart cards and transport systems.