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.

• Type: Conference
• Year: 2003
• Where: FM
• Authors: Michael Leuschel, Michael J. Butler
• Keywords: FM 2003, Model Checking Tool, ProB Enables Users, ProB’s Animation Facilities