ProB Validation Methods

Revision as of 09:00, 16 January 2015 by Michael Leuschel (talk | contribs)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

ProB offers various validation techniques:

Here we want to describe the advantages and disadvantages of the various methods.

Comparing ProB Validation Techniques
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