Created page with ' ProB offers various validation techniques: * Consistency Checking (Finding Invariant Violations using the Model Checker) * [[Constraint Based Checking]…' |
No edit summary |
||
| (3 intermediate revisions by the same user not shown) | |||
| Line 1: | Line 1: | ||
ProB offers various validation techniques: | ProB offers various validation techniques: | ||
| Line 12: | Line 11: | ||
{| border="1" | {| border="1" | ||
|+ align="bottom" style="color:#e76700;" |'' | |+ align="bottom" style="color:#e76700;" |''Comparing ProB Validation Techniques'' | ||
! Question | |||
! Model Checking | ! Model Checking | ||
! LTL Model Checking | ! LTL Model Checking | ||
| Line 20: | Line 20: | ||
| Can find Invariant Violations ? | | Can find Invariant Violations ? | ||
| yes | | yes | ||
| yes | | yes (<tt>G{INV}</tt>) | ||
| yes | | yes | ||
| yes | | yes | ||
| Line 29: | Line 29: | ||
|no | |no | ||
| yes | | yes | ||
|- | |||
| Search Technique for counter-examples? | |||
| mixed df/bf, df, bf | |||
| depth-first (df) | |||
| length 1 | |||
| breadth-first (bf) | |||
|- | |- | ||
| Can deal with large branching factor? | | Can deal with large branching factor? | ||
| Line 44: | Line 50: | ||
| Can find deadlocks ? | | Can find deadlocks ? | ||
| yes | | yes | ||
| yes (G not | | yes (<tt>G not(deadlock)</tt>) | ||
| yes | | yes | ||
| not yet | | not yet | ||
| Line 50: | Line 56: | ||
| Can find assertion violations ? | | Can find assertion violations ? | ||
| yes | | yes | ||
| | | (<tt>G{ASS}</tt>) | ||
| static | | static | ||
| no | | no | ||
ProB offers various validation techniques:
Here we want to describe the advantages and disadvantages of the various methods.
| Question | Model Checking | LTL Model Checking | CBC Checking | Bounded Model Checking |
|---|---|---|---|---|
| Can find Invariant Violations ? | yes | yes (G{INV}) | yes | yes |
| Only reachable counter-examples from initial state? | yes | yes | no | yes |
| Search Technique for counter-examples? | mixed df/bf, df, bf | depth-first (df) | length 1 | breadth-first (bf) |
| Can deal with large branching factor? | no | no | yes | yes |
| Can find deep counter-examples? | yes | yes | n/a (length 1) | no |
| Can find deadlocks ? | yes | yes (G not(deadlock)) | yes | not yet |
| Can find assertion violations ? | yes | (G{ASS}) | static | no |
| Can confirm absence of errors ? | finite statespace | finite statespace | invariant strong enough | bound on trace length |