ProB Validation Methods - Revision history

Michael Leuschel at 09:00, 16 January 2015

2015-01-16T09:00:53Z

← Older revision		Revision as of 09:00, 16 January 2015
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

Michael Leuschel at 09:00, 16 January 2015

2015-01-16T09:00:29Z

← Older revision		Revision as of 09:00, 16 January 2015
Line 20:		Line 20:
	\| Can find Invariant Violations ?		\| Can find Invariant Violations ?
	\| yes		\| yes
	\| yes		\| yes (<tt>G {INV}</tt>)
	\| yes		\| yes
	\| yes		\| yes
Line 50:		Line 50:
	\| Can find deadlocks ?		\| Can find deadlocks ?
	\| yes		\| yes
	\| yes (G not {deadlock})		\| yes (<tt>G not(deadlock)</tt>)
	\| yes		\| yes
	\| not yet		\| not yet
Line 56:		Line 56:
	\| Can find assertion violations ?		\| Can find assertion violations ?
	\| yes		\| yes
	\| no		\| (<tt>G {ASS}</tt>)
	\| static		\| static
	\| no		\| no

Michael Leuschel at 08:59, 16 January 2015

2015-01-16T08:59:02Z

← Older revision		Revision as of 08:59, 16 January 2015
Line 29:		Line 29:
	\|no		\|no
	\| yes		\| 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?		\| Can deal with large branching factor?

Michael Leuschel at 08:56, 16 January 2015

2015-01-16T08:56:45Z

← Older revision		Revision as of 08:56, 16 January 2015
Line 1:		Line 1:

	ProB offers various validation techniques:		ProB offers various validation techniques:

Line 12:		Line 11:

	{\| border="1"		{\| border="1"
	\|+ align="bottom" style="color:#e76700;" \|''~~Question~~''		\|+ align="bottom" style="color:#e76700;" \|''Comparing ProB Validation Techniques''
			! Question
	! Model Checking		! Model Checking
	! LTL Model Checking		! LTL Model Checking

Michael Leuschel: Created page with ' ProB offers various validation techniques: * Consistency Checking (Finding Invariant Violations using the Model Checker) * [[Constraint Based Checking]…'

2015-01-16T08:56:10Z

Created page with ' ProB offers various validation techniques: * Consistency Checking (Finding Invariant Violations using the Model Checker) * [[Constraint Based Checking]…'

New page

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;" |''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
|}