What is ProB? ProB is an animator and model checker for the B-Method. It allows animation of many B specifications, and can be used to systematically check a specification for a range of errors. The constraint-solving capabilities of ProB can also be used for model finding, deadlock checking and test-case generation.

Components

ProB Cli

The ProB CLI provides access to the features of ProB via command line. Hence, you can run ProB from your shell scripts or in your Makefiles.

ProB Tcl/Tk

The ProB Tcl/Tk application provides a user interface for ProB for the verification of B, Event-B, CSP-M, TLA+ and Z specifications via animation and model checking.

ProB Java API

The ProB Java API makes the functionality of ProB available via an API that can be easily integrated into any existing Java application. The library also provides support for the Groovy scripting language, which allows users to direct animations and model checking via scripting.

BMotion Studio

BMotion Studio is a tool build on top of the ProB Java API for creating domain specific visualisations of formal models.

ProB for Rodin

ProB for Rodin is a plug-in that enables Event-B models to be animated and verified from within the Rodin IDE.

ProB for TLA

ProB for TLA provides a convenient way to use ProB as a new validation tool for TLA+. There is also a plug-in for the TLA toolbox.

Getting Started

ProB Cli

Tutorial

User Manual

Developer Manual

ProB Tcl/Tk

Tutorial

User Manual

Developer Manual

ProB Java API

Tutorial

User Manual

Developer Manual

BMotion Studio

Tutorial

User Manual

Developer Manual

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 visualized. ProB also supports Z specifications (ProB in this context is sometimes called ProZ) as well as TLA+ specifications. We now also have an online ProB Logic Calculator.