No edit summary |
No edit summary |
||
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? |
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 | 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 | no | static | no |
Can confirm absence of errors ? | finite statespace | finite statespace | invariant strong enough | bound on trace length |