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 |