Tutorial

ProB is a flexible and extensible validation tool for high-level specification formalisms. ProB supports

• multiple languages: B, Z, CSP, Event-B, Promela, dSL, ...
• and multiple validation techniques
: animation, model checking, ...

Below we present a gentle introduction to ProB focusing on classical B (but many of the commands are also applicable to the other formalisms such as CSP, Event-B and Z).

• Starting ProB and first animation steps
• First steps in model checking
• Complete model checking
• How to tune model checking

Understanding ProB's Animation and Constraint Solving along with Tips:

• Understanding the ProB Setup Phases
• Some animation tips (dealing with large parameter values,...)
• Tutorial Troubleshooting the Setup
• Tutorial Understanding the Complexity of B Animation
• Tutorial Understanding ProB's Constraint Solver
• Tutorial Debugging Well-Definedness and Transition Errors
• Tips for Large Specifications

Advanced Validation with ProB:

• Directed model checking
• Tutorial Enabling Analysis
• Tutorial Various Optimizations
• Model Checking, Proof and Constraint-Based Checking
• Tutorial on Model-Based Testing

Other Tutorials:

• Tutorial on using the Evaluation View
• Tutorial on using the Eval Console
• Tutorial Modeling Infinite Datatypes
• Some Example Specifications and their Validation with ProB

For ProB for Rodin, the following presents a gentle introduction:

• Starting ProB for Rodin and first animation steps
• Important Parameters of ProB for Rodin
• Exporting Rodin Models for ProB Classic
• Using the Symbolic Contants Plugin
• Using the ProB (Dis-)Prover
• Visualization of LTL Counter-examples in Rodin

The Rodin handbook also contains material about ProB:

• Finding Invariant Violations with ProB
• Finding Solutions to Axioms

For ProB for CSP, the following presents a gentle introduction:

• Starting ProB for CSP and first animation steps

The following tutorials concern older versions of ProB.

There are two tutorials on the physical units plugin (which is no longer supported as of ProB 1.9.0):

• Using the Physical Units Plugin inside ProB
• Analysing Physical Units with ProB for Rodin

For Co-Simulation we have this tutorial:

• Tutorial Co-Simulation

We also have a tutorial for B Motion Studio, but we now recommend you use VisB instead.

Feedback

Please help us to improve this documentation by providing feedback in our bug tracker, asking questions in our prob-users group or sending an email to Michael Leuschel.