No edit summary |
No edit summary |
||
| Line 5: | Line 5: | ||
* [[Graphical Visualization]] | * [[Graphical Visualization]] | ||
* [[State Space Visualization]] | * [[State Space Visualization]] | ||
Validation with ProB: | |||
* [[Consistency Checking|Consistency Checking (Finding Invariant Violations using the Model Checker)]] | * [[Consistency Checking|Consistency Checking (Finding Invariant Violations using the Model Checker)]] | ||
* [[Constraint Based Checking]] | * [[Constraint Based Checking]] | ||
| Line 12: | Line 14: | ||
* [[Symbolic Model Checking|Symbolic Model Checking]] | * [[Symbolic Model Checking|Symbolic Model Checking]] | ||
* [[ProB Validation Methods|Comparing the various ProB Validation Methods]] | * [[ProB Validation Methods|Comparing the various ProB Validation Methods]] | ||
Other Interfaces to ProB: | |||
* [[Using the Command-Line Version of ProB]] | |||
* [[ProB2_JavaFX_UI|ProB2 JavaFX User Interface]] | |||
ProB and Other Tools: | |||
* [[Using ProB with Atelier B]] | * [[Using ProB with Atelier B]] | ||
* [[TLC|Using TLC for B Specifications]] | |||
* [[Using ProB with KODKOD]] | |||
* [[Using ProB with Z3]] | |||
* [[Editors for ProB]] | |||
ProB for Other Languages: | |||
* [[CSP-M|Using CSP-M in ProB]] | * [[CSP-M|Using CSP-M in ProB]] | ||
* [[Checking CSP Assertions]] | * [[Checking CSP Assertions]] | ||
| Line 19: | Line 34: | ||
* [[ProZ|Using ProZ for Animation and Model Checking of Z Specifications]] | * [[ProZ|Using ProZ for Animation and Model Checking of Z Specifications]] | ||
* [[TLA|Using ProB for TLA Specifications]] | * [[TLA|Using ProB for TLA Specifications]] | ||
* [[Alloy|Using ProB for Alloy Specifications]] | * [[Alloy|Using ProB for Alloy Specifications]] | ||
* [[Other languages|Using ProB with Promela and other languages]] | * [[Other languages|Using ProB with Promela and other languages]] | ||
Advanced Features of ProB: | |||
* [[Symmetry Reduction]] | * [[Symmetry Reduction]] | ||
* [[ParB|Parallel Execution of ProB]] | * [[ParB|Parallel Execution of ProB]] | ||
| Line 30: | Line 46: | ||
* [[Test Case Generation]] | * [[Test Case Generation]] | ||
* [[State Space Coverage Analyses]] | * [[State Space Coverage Analyses]] | ||
* [[Generating Documents with ProB and Latex]] | * [[Generating Documents with ProB and Latex]] | ||
FAQ, Tips and Troubleshootings: | |||
* [[FAQ]] | * [[FAQ]] | ||
* [[Controlling_ProB_Preferences|Setting ProB Preferences]] | * [[Controlling_ProB_Preferences|Setting ProB Preferences]] | ||
| Line 39: | Line 54: | ||
* [[Tips: Writing Models for ProB]] | * [[Tips: Writing Models for ProB]] | ||
* [[Tips: B Idioms|Tips: Common B Idioms (let, if-then-else,...)]] | * [[Tips: B Idioms|Tips: Common B Idioms (let, if-then-else,...)]] | ||
* [[Summary of B Syntax]] | * [[Summary of B Syntax]] | ||
* [[Well-Definedness Checking]] | * [[Well-Definedness Checking]] | ||
Validation with ProB:
Other Interfaces to ProB:
ProB and Other Tools:
ProB for Other Languages:
Advanced Features of ProB:
FAQ, Tips and Troubleshootings: