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.
Keywords for this software
References in zbMATH (referenced in 6 articles , 1 standard article )
Showing results 1 to 6 of 6.
- Leuschel, Michael; Falampin, Jér^ome; Fritz, Fabian; Plagge, Daniel: Automated property verification for large scale B models with ProB (2011)
- Plagge, Daniel; Leuschel, Michael: Seven at one stroke: LTL model checking for high-level specifications in B, Z, CSP, and more (2010)
- Leuschel, Michael; Butler, Michael: Prob: An automated analysis toolset for the B method (2008)
- Bouquet, Fabrice; Legeard, Bruno; Peureux, Fabien: CLPS --- B --- A constraint solver to animate a B specification (2004)
- Katoen, Joost-Pieter; Stevens, Perdita: Guest editors’ introduction: advancements and extensions of verification techniques (2004)
- Bouquet, Fabrice; Legeard, Bruno; Peureux, Fabien: CLPS-B -- a constraint solver for B (2002)