BETA: a B basEd Testing Approach

Intro

BETA is a tool supported approach to generate unit tests from B specifications. The tool receives as input the specification of an abstract B machine and automatically generates a report with test input data for selected operations. The tool is free, cross-platform and open-source.

Motivation

While formal methods provide ways to specify and verify software systems with mathematical accuracy, testing techniques can provide mechanisms to identify defects that were inserted in the system during its implementation. With that in mind, we developed an approach and a tool to generate test specifications based on a formal notation: the B-Method. Our approach uses restrictions described on a B specification, such as invariants, preconditions and conditional statements, to create unit tests for an operation. The approach uses equivalence classes and boundary value analysis techniques to partition the operation input space and relies on combinatorial criteria (such as all-combinations, each-choice and pairwise) to select partitions to test.