Sciweavers

FM
2003
Springer

ProB: A Model Checker for B

13 years 8 months ago
ProB: A Model Checker for B
We present ProB, an animation and model checking tool for the B method. ProB’s animation facilities allow users to gain confidence in their specifications, and unlike the animator provided by the B-Toolkit, the user does not have to guess the right values for the operation arguments or choice variables. ProB contains a model checker and a constraint-based checker, both of which can be used to detect various errors in B specifications. We present our first experiences in using ProB on several case studies, highlighting that ProB enables users to uncover errors that are not easily discovered by existing tools.
Michael Leuschel, Michael J. Butler
Added 06 Jul 2010
Updated 06 Jul 2010
Type Conference
Year 2003
Where FM
Authors Michael Leuschel, Michael J. Butler
Comments (0)