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 10 articles , 1 standard article )
Showing results 1 to 10 of 10.
- Leuschel, Michael; Falampin, Jér^ome; Fritz, Fabian; Plagge, Daniel: Automated property verification for large scale B models with ProB (2011)
- Blanc, Benjamin; Junke, Christophe; Marre, Bruno; Le Gall, Pascale; Andrieu, Olivier: Handling state-machines specifications with gatel (2010)
- Plagge, Daniel; Leuschel, Michael: Seven at one stroke: LTL model checking for high-level specifications in B, Z, CSP, and more (2010)
- Dadeau, Frédéric; Levrey, Jocelyn; Héam, Pierre-Cyrille: On the use of uniform random generation of automata for testing (2009)
- Dadeau, Frédéric; Tissot, Régis: Jsynopsys - A scenario-based testing tool based on the symbolic animation of B machines (2009)
- 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)
- Couchot, Jean-Francois; Dadeau, Frédéric; Déharbe, David; Giorgetti, Alain; Ranise, Silvio: Proving and debugging set-based specifications. (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)