Tutorial: Difference between revisions

No edit summary
No edit summary
 
(40 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, 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).
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 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 Understanding the Complexity of B Model Checking]]
* [[Tutorial Debugging Well-Definedness and Transition Errors]]
* [[Tips for Large Specifications]]
 
Advanced Validation with ProB:


* [[Using the Command-Line Version of 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 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:
For ProB for CSP, the following presents a gentle introduction:


* [[Tutorial CSP First Step|Starting ProB for CSP and first animation steps]]
* [[Tutorial CSP First Step|Starting ProB for CSP and first animation steps]]


We also have a [http://www.stups.uni-duesseldorf.de/BMotionStudio/tutorials.php tutorial for B Motion Studio].
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}}

Latest revision as of 16:21, 2 October 2021


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).

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.

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.