Tutorial: Difference between revisions
No edit summary |
No edit summary |
||
| Line 17: | Line 17: | ||
* [[Tutorial Understanding the Complexity of B Model Checking]] | * [[Tutorial Understanding the Complexity of B Model Checking]] | ||
* [[Tutorial Debugging Well-Definedness and Transition Errors]] | * [[Tutorial Debugging Well-Definedness and Transition Errors]] | ||
* [[Tutorial on using the Evaluation View|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]] | ||
Revision as of 12:04, 7 October 2011
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
- Understanding the ProB Setup Phases
- Tutorial Troubleshooting the Setup
- Tutorial Understanding the Complexity of B Animation
- Tutorial Understanding ProB's Constraint Solver
- Tutorial Understanding the Complexity of B Model Checking
- Tutorial Debugging Well-Definedness and Transition Errors
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.