Tutorial: Difference between revisions

No edit summary
No edit summary
 
(5 intermediate revisions by the same user not shown)
Line 10: Line 10:


* [[Tutorial First Step|Starting ProB and first animation steps]]
* [[Tutorial First Step|Starting ProB and first animation steps]]
* [[Tutorial Animation Tips|Some animation tips (dealing with large parameter values,...)]]
* [[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 Directed Model Checking|Directed 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 Debugging Well-Definedness and Transition Errors]]
* [[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 Enabling Analysis]]
* [[Tutorial Model Checking with Various Optimizations|Tutorial Various Optimizations]]
* [[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]]
* [[Evaluation View|Tutorial on using the Evaluation View]]
* [[Eval Console|Tutorial on using the Eval Console]]
* [[Eval Console|Tutorial on using the Eval Console]]
* [[Tutorial Model Checking, Proof and CBC|Model Checking, Proof and Constraint-Based Checking]]
* [[Tutorial Model-Based Testing|Tutorial on Model-Based Testing]]
* [[Using the Command-Line Version of ProB]]
* [[Tutorial Modeling Infinite Datatypes]]
* [[Tutorial Modeling Infinite Datatypes]]
*[[Tutorial Co-Simulation]]
* [[ProB Examples|Some Example Specifications and their Validation with ProB]]
* [[ProB Examples|Some Example Specifications and their Validation with ProB]]


Line 46: Line 47:
* [[Tutorial LTL Counter-example View| Visualization of LTL Counter-examples in Rodin]]
* [[Tutorial LTL Counter-example View| Visualization of LTL Counter-examples in Rodin]]


The [http://handbook.event-b.org Rodin handbook] also contains material about ProB:
The [https://www3.hhu.de/stups/handbook/rodin/current/html/index.html Rodin handbook] also contains material about ProB:
* [http://handbook.event-b.org/current/html/tut_building_the_model.html#tut:prob  Finding Invariant Violations with ProB]
* [https://www3.hhu.de/stups/handbook/rodin/current/html/tut_building_the_model.html#tut:prob  Finding Invariant Violations with ProB]
* [http://handbook.event-b.org/current/html/tut_populate_context.html#a0000000094 Finding Solutions to Axioms]
* [https://www3.hhu.de/stups/handbook/rodin/current/html/tut_populate_context.html#a0000000094 Finding Solutions to Axioms]


Furthermore, there are several tutorials on the physical units plugin:
* [[Tutorial Unit Plugin|Using the Physical Units Plugin inside ProB]]
* [[Tutorial Unit Plugin With Rodin|Analysing Physical Units with ProB for Rodin]]


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


{{Feedback}}
{{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.