CLPS-B - A constraint solver for B

Abstract

This paper proposes an approach to the evaluation of B formal specifications using Constraint Logic Programming with sets. This approach is used to animate and generate test sequences from B formal specifications. The solver, called CLPS-B, is described in terms of constraint domains, consistency verification and constraint propagation. It is more powerful than most constraint systems, because it allows the domain of variable to contain other variables, which increase the level of abstraction. The constrained state propagates the non-determinism of the B specifications and reduces the number of states in a reachability graph. We illustrate this approach by comparing the constrained states graph exploration with the concrete one in a simple example: Process scheduler. © Springer-Verlag Berlin Heidelberg 2002.