ProB Validation Methods

ProB offers various validation techniques:

• Consistency Checking (Finding Invariant Violations using the Model Checker)
• Constraint Based Checking
• Refinement Checking
• LTL Model Checking
• Bounded Model Checking

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
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