No edit summary |
No edit summary |
||
| Line 20: | Line 20: | ||
| Can find Invariant Violations ? | | Can find Invariant Violations ? | ||
| yes | | yes | ||
| yes (<tt>G {INV}</tt>) | | yes (<tt>G{INV}</tt>) | ||
| yes | | yes | ||
| yes | | yes | ||
| Line 56: | Line 56: | ||
| Can find assertion violations ? | | Can find assertion violations ? | ||
| yes | | yes | ||
| (<tt>G {ASS}</tt>) | | (<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 |