No edit summary |
No edit summary |
||
| (44 intermediate revisions by 6 users not shown) | |||
| Line 1: | Line 1: | ||
[[Category:Tutorial]] | [[Category:Tutorial]] | ||
[[Category:ProB Tcl Tk]] | |||
ProB is a flexible and extensible validation tool for high-level specification formalisms. | ProB is a flexible and extensible validation tool for high-level specification formalisms. | ||
| Line 6: | Line 7: | ||
* and multiple validation techniques
: animation, model checking, ... | * and multiple validation techniques
: animation, model checking, ... | ||
Below | 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). | ||
* [[Tutorial First Step|Starting ProB and first animation steps]] | * [[Tutorial First Step|Starting ProB and first animation steps]] | ||
* [[Tutorial First Model Checking|First steps in model checking]] | * [[Tutorial First Model Checking|First steps in model checking]] | ||
* [[Tutorial Complete Model Checking|Complete model checking]] | |||
* [[Tutorial Tuning Model Checking|How to tune model checking]] | |||
Understanding ProB's Animation and Constraint Solving along with Tips: | |||
* [[Tutorial Setup Phases|Understanding the ProB Setup Phases]] | * [[Tutorial Setup Phases|Understanding the ProB Setup Phases]] | ||
* [[Tutorial Animation Tips|Some animation tips (dealing with large parameter values,...)]] | |||
* [[Tutorial Troubleshooting the Setup]] | * [[Tutorial Troubleshooting the Setup]] | ||
* [[Tutorial Understanding the Complexity of B Animation]] | * [[Tutorial Understanding the Complexity of B Animation]] | ||
* [[Tutorial Understanding ProB's Constraint Solver]] | * [[Tutorial Understanding ProB's Constraint Solver]] | ||
* [[Tutorial | * [[Tutorial Debugging Well-Definedness and Transition Errors]] | ||
* [[Tips for Large Specifications]] | |||
Advanced Validation with ProB: | |||
* [[ | * [[Tutorial Directed Model Checking|Directed model checking]] | ||
* [[Tutorial Enabling Analysis]] | |||
* [[Tutorial Model Checking with Various Optimizations|Tutorial Various Optimizations]] | |||
* [[Tutorial Model Checking, Proof and CBC|Model Checking, Proof and Constraint-Based Checking]] | |||
* [[Tutorial Model-Based Testing|Tutorial on Model-Based Testing]] | |||
Other Tutorials: | |||
* [[Evaluation View|Tutorial on using the Evaluation View]] | |||
* [[Eval Console|Tutorial on using the Eval Console]] | |||
* [[Tutorial Modeling Infinite Datatypes]] | |||
* [[ProB Examples|Some Example Specifications and their Validation with ProB]] | |||
For ProB for Rodin the following presents a gentle introduction: | For ProB for Rodin, the following presents a gentle introduction: | ||
* [[Tutorial Rodin First Step|Starting ProB for Rodin and first animation steps]] | * [[Tutorial Rodin First Step|Starting ProB for Rodin and first animation steps]] | ||
* [[Tutorial Rodin Parameters|Important Parameters of ProB for Rodin]] | |||
* [[Tutorial Rodin Exporting|Exporting Rodin Models for ProB Classic]] | |||
* [[Tutorial Symbolic Constants|Using the Symbolic Contants Plugin]] | |||
* [[Tutorial Disprover|Using the ProB (Dis-)Prover]] | |||
* [[Tutorial LTL Counter-example View| Visualization of LTL Counter-examples in Rodin]] | |||
The [https://www3.hhu.de/stups/handbook/rodin/current/html/index.html Rodin handbook] also contains material about ProB: | |||
* [https://www3.hhu.de/stups/handbook/rodin/current/html/tut_building_the_model.html#tut:prob Finding Invariant Violations with ProB] | |||
* [https://www3.hhu.de/stups/handbook/rodin/current/html/tut_populate_context.html#a0000000094 Finding Solutions to Axioms] | |||
For ProB for CSP, the following presents a gentle introduction: | |||
* [[Tutorial CSP First Step|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): | |||
* [[Tutorial Unit Plugin|Using the Physical Units Plugin inside ProB]] | |||
* [[Tutorial Unit Plugin With Rodin|Analysing Physical Units with ProB for Rodin]] | |||
For Co-Simulation we have this tutorial: | |||
*[[Tutorial Co-Simulation]] | |||
We also have a [http://www.stups.uni-duesseldorf.de/bmotionstudio/index.php/User_Guide/Tutorial tutorial for B Motion Studio]. | |||
{{Feedback}} | |||
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).
Understanding ProB's Animation and Constraint Solving along with Tips:
Advanced Validation with ProB:
Other Tutorials:
For ProB for Rodin, the following presents a gentle introduction:
The Rodin handbook also contains material about ProB:
For ProB for CSP, the following presents a gentle introduction:
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):
For Co-Simulation we have this tutorial:
We also have a tutorial for B Motion Studio.
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.