No edit summary |
No edit summary |
||
Line 18: | Line 18: | ||
* [[Tutorial Debugging Well-Definedness and Transition Errors]] | * [[Tutorial Debugging Well-Definedness and Transition Errors]] | ||
* [[Tutorial on using the | * [[Evaluation View|Tutorial on using the Evaluation View]] | ||
* [[Tutorial Model Checking, Proof and CBC|Model Checking, Proof and Constraint-Based Checking]] | * [[Tutorial Model Checking, Proof and CBC|Model Checking, Proof and Constraint-Based Checking]] |
ProB is a flexible and extensible validation tool for high-level specification formalisms.
ProB supports
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).
For ProB for Rodin, the following presents a gentle introduction:
For ProB for CSP, the following presents a gentle introduction:
We also have a tutorial for B Motion Studio.