View source for ProB Validation Methods

ProB offers various validation techniques:

* [[Consistency Checking|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.


{| border="1"
|+ align="bottom" style="color:#e76700;" |''Comparing ProB Validation Techniques''
!  Question
!  Model Checking
! LTL Model Checking
! CBC Checking
! Bounded Model Checking
|-
| Can find Invariant Violations ?
| yes
| yes (<tt>G{INV}</tt>)
| 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 (<tt>G not(deadlock)</tt>)
| yes
| not yet
|-
 | Can find assertion violations ?
| yes
|  (<tt>G{ASS}</tt>)
| static 
| no
|-
 | Can confirm absence of errors ?
| finite statespace
| finite statespace
| invariant strong enough
| bound on trace length
|}