The ProB Animator and Model Checker for the B Method

ProB is an animator and model checker for the B-Method (see the B Site Pages, B-Method site of Clearsy, or the B Formal Methods Virtual Library). It allows fully automatic animation of many B specifications, and can be used to systematically check a specification for errors. In addition to B, ProB now also supports CSP-M and Z. Part of the research and development was conducted within the EPSRC funded projects ABCD and iMoc, and within the EU funded project Rodin. Development is continued under the EU funded project Deploy and the DFG project Gepavas. ProB has been successfully used on various industrial specifications (e.g., from Nokia Research).

The Implementation

The core of ProB is implemented in SICStus Prolog (but can be run without a SICStus Prolog license). It uses co-routining and finite domain constraint solving to make animation of B machines possible.

Features

ProB covers a large part of B, and we are striving towards full coverage of Atelier B and B4Free constructs. ProB supports B features such as non-deterministic operations, ANY statements, operations with complex arguments, sets, sequences, functions, lambda abstractions, set comprehensions, records, constants and properties, and many more. Not supported are the Atelier B tree operations and there are restrictions on DEFINITIONS. ProB does support multiple machines, refinements, and implementations. ProB can also be used for automated refinement checking and LTL model checking. It also supports almost full CSP-M process descriptions (as of version 1.2.7), to be used on their own or to guide B machines for specification and property validation. The state space of the specifications can be graphically visualised.

Some Screenshots

Screenshots can be found here.

Related Products

Upcoming Features

We are working on:
  • Eclipse version integrated with BE4 Editor (scheduled for 2009)
  • New parser and typechecker with better support for DEFINITIONS and almost full compliance with Atelier B (now released)
  • Integration into Atelier-B 4.0 (already released; support for checking individual proof obligations is up and coming)
  • Multi-level animation for Event-B models (available in 1.3.1)
  • B Motion Studio for generating and editing graphical visualizations (beta version available)
  • Integration of full finite-domain constraint solving for integers; Kodkod integration.
  • Directed model checking, model-based testing.