State Space Coverage Analyses - Revision history

Michael Leuschel at 12:37, 3 September 2015

2015-09-03T12:37:54Z

← Older revision		Revision as of 12:37, 3 September 2015
Line 16:		Line 16:
	* Precise Operation Coverage: will check which operations have been covered in the current state space; for those operations that have not been covered, the constraint solver is called to determine whether the operation is actually feasible given the invariant (is there a state satisfying the invariant which enables the operation). If an operation is infeasible, it can never be reached (unless we reach a state violating the invariant).		* Precise Operation Coverage: will check which operations have been covered in the current state space; for those operations that have not been covered, the constraint solver is called to determine whether the operation is actually feasible given the invariant (is there a state satisfying the invariant which enables the operation). If an operation is infeasible, it can never be reached (unless we reach a state violating the invariant).

			The commands to determine vacuous guards and invariants rely on MC/DC coverage, which is detailed below.

	~~== Operation/Event Coverage ==~~

	~~[TO DO]~~

	== MC/DC Coverage ==		== MC/DC Coverage ==

Michael Leuschel at 12:36, 3 September 2015

2015-09-03T12:36:50Z

← Older revision		Revision as of 12:36, 3 September 2015
Line 6:		Line 6:

	These coverage commands all operate on the <b>state space</b> of the B model, i.e., those states that ProB has visited via animation or model checking from the initial states. Note: if you perform constraint-based checks, ProB may add additional states to this state space, which are not necessarily reachable from the initial states. Note: these commands do not drive the model checker and work on the currently explored state space; if the state space is incomplete the commands may obviously miss covered values in the unexplored part.		These coverage commands all operate on the <b>state space</b> of the B model, i.e., those states that ProB has visited via animation or model checking from the initial states. Note: if you perform constraint-based checks, ProB may add additional states to this state space, which are not necessarily reachable from the initial states. Note: these commands do not drive the model checker and work on the currently explored state space; if the state space is incomplete the commands may obviously miss covered values in the unexplored part.
			Finally, the larger the state space, the more time these commands will take.

	Here is a brief overview of the main commands:		Here is a brief overview of the main commands:
Line 12:		Line 13:
	* Minimum and Maximum Values: determine for each variable and constant a minumum and maximum value that is reached. This also detects whether just a single value was encountered. This command is particularly useful when model checking unexpectedly runs for very long or seems to run forever: here one can often spot individual variables which grow in an unbounded fashion.		* Minimum and Maximum Values: determine for each variable and constant a minumum and maximum value that is reached. This also detects whether just a single value was encountered. This command is particularly useful when model checking unexpectedly runs for very long or seems to run forever: here one can often spot individual variables which grow in an unbounded fashion.
	* Value coverage for Expression: this allows the user to enter an expression, which is computed in every state of the state space; all values are then displayed in a table along with the possible values, how often these values have been encountered and a witness state id, giving you one possible witness state for this value.		* Value coverage for Expression: this allows the user to enter an expression, which is computed in every state of the state space; all values are then displayed in a table along with the possible values, how often these values have been encountered and a witness state id, giving you one possible witness state for this value.
			* Number of covered values for variables: computes for each variable, how many different values it has taken on in the state space. Again, this is useful to diagnose state space explosion.
			* Precise Operation Coverage: will check which operations have been covered in the current state space; for those operations that have not been covered, the constraint solver is called to determine whether the operation is actually feasible given the invariant (is there a state satisfying the invariant which enables the operation). If an operation is infeasible, it can never be reached (unless we reach a state violating the invariant).

Michael Leuschel at 12:31, 3 September 2015

2015-09-03T12:31:36Z

← Older revision		Revision as of 12:31, 3 September 2015
Line 4:		Line 4:

	[[file:CoverageMenu.png\|center\|\|300px]]		[[file:CoverageMenu.png\|center\|\|300px]]

			These coverage commands all operate on the <b>state space</b> of the B model, i.e., those states that ProB has visited via animation or model checking from the initial states. Note: if you perform constraint-based checks, ProB may add additional states to this state space, which are not necessarily reachable from the initial states. Note: these commands do not drive the model checker and work on the currently explored state space; if the state space is incomplete the commands may obviously miss covered values in the unexplored part.

			Here is a brief overview of the main commands:

			* Operation Coverage: determine which operations (aka events for Event-B or actions for TLA) are covered in the state-space and compute how often each operation is enabled
			* Minimum and Maximum Values: determine for each variable and constant a minumum and maximum value that is reached. This also detects whether just a single value was encountered. This command is particularly useful when model checking unexpectedly runs for very long or seems to run forever: here one can often spot individual variables which grow in an unbounded fashion.
			* Value coverage for Expression: this allows the user to enter an expression, which is computed in every state of the state space; all values are then displayed in a table along with the possible values, how often these values have been encountered and a witness state id, giving you one possible witness state for this value.

Michael Leuschel: /* MC/DC Coverage */

2015-09-02T06:46:20Z

MC/DC Coverage

← Older revision		Revision as of 06:46, 2 September 2015
Line 14:		Line 14:
	MC/DC (Modified Condition/Decision Coverage) is a coverage criterion which is used in avionics. One core idea is ensure that for every condition in our code or model we generate at least one test where the condition independently plays an observable role in the outcome of a decision. In other words, if the condition were to be true rather than false (or vice versa) the decision would be changed. In still other words, we are trying to find an execution context where the result of the particular condition under test is crucial for the observable outcome.		MC/DC (Modified Condition/Decision Coverage) is a coverage criterion which is used in avionics. One core idea is ensure that for every condition in our code or model we generate at least one test where the condition independently plays an observable role in the outcome of a decision. In other words, if the condition were to be true rather than false (or vice versa) the decision would be changed. In still other words, we are trying to find an execution context where the result of the particular condition under test is crucial for the observable outcome.

	In the context of B and Event-B, one question is what constitutes a condition and what constitutes a decision. ~~In WP4 we~~ view a condition to be an atomic predicate (e.g., x>y) not involving logical connectives (<tt>&</tt>, <tt>or</tt>, <tt>not</tt>, <tt>=></tt>, ⇔). There is, however, the possibility of treating a bigger predicate as atomic (e.g., an entire guard of an event). The reason for this is to provide better feedback to the user and to reduce the number of coverage criteria if desired. At the moment, we also consider a universally or existentially quantified formula to be a condition.		In the context of B and Event-B, one question is what constitutes a condition and what constitutes a decision. We view a <b>condition</b> to be an atomic predicate (e.g., x>y) not involving logical connectives (<tt>&</tt>, <tt>or</tt>, <tt>not</tt>, <tt>=></tt>, ⇔). There is, however, the possibility of treating a bigger predicate as atomic (e.g., an entire guard of an event). The reason for this is to provide better feedback to the user and to reduce the number of coverage criteria if desired. At the moment, we also consider a universally or existentially quantified formula to be a condition.
	A decision constitutes the fact whether an event is enabled or not. However, we also ~~enable~~ MC/DC to be applied in other contexts, e.g., to analyse invariants; in that setting a decision is whether an invariant is true or false.		A <b>decision</b> constitutes the fact whether an event is enabled or not. However, we also allow MC/DC to be applied in other contexts, e.g., to analyse invariants; in that setting a decision is whether an invariant is true or false.

	We have implemented a MC/DC coverage analysis which examines all visited states and computes the MC/DC coverage for a series of predicates under consideration.		We have implemented a MC/DC coverage analysis which examines all visited states and computes the MC/DC coverage for a series of predicates under consideration.

Michael Leuschel: /* MC/DC Coverage */

2015-09-02T06:43:21Z

MC/DC Coverage

← Older revision		Revision as of 06:43, 2 September 2015
Line 14:		Line 14:
	MC/DC (Modified Condition/Decision Coverage) is a coverage criterion which is used in avionics. One core idea is ensure that for every condition in our code or model we generate at least one test where the condition independently plays an observable role in the outcome of a decision. In other words, if the condition were to be true rather than false (or vice versa) the decision would be changed. In still other words, we are trying to find an execution context where the result of the particular condition under test is crucial for the observable outcome.		MC/DC (Modified Condition/Decision Coverage) is a coverage criterion which is used in avionics. One core idea is ensure that for every condition in our code or model we generate at least one test where the condition independently plays an observable role in the outcome of a decision. In other words, if the condition were to be true rather than false (or vice versa) the decision would be changed. In still other words, we are trying to find an execution context where the result of the particular condition under test is crucial for the observable outcome.

	In the context of B and Event-B, one question is what constitutes a condition and what constitutes a decision. In WP4 we view a condition to be an atomic predicate (e.g., x>y) not involving logical connectives (<tt>&</tt>, <tt>or</tt>, </tt>not</tt>, <tt>=></tt>, ⇔). There is, however, the possibility of treating a bigger predicate as atomic (e.g., an entire guard of an event). The reason for this is to provide better feedback to the user and to reduce the number of coverage criteria if desired. At the moment, we also consider a universally or existentially quantified formula to be a condition.		In the context of B and Event-B, one question is what constitutes a condition and what constitutes a decision. In WP4 we view a condition to be an atomic predicate (e.g., x>y) not involving logical connectives (<tt>&</tt>, <tt>or</tt>, <tt>not</tt>, <tt>=></tt>, ⇔). There is, however, the possibility of treating a bigger predicate as atomic (e.g., an entire guard of an event). The reason for this is to provide better feedback to the user and to reduce the number of coverage criteria if desired. At the moment, we also consider a universally or existentially quantified formula to be a condition.
	A decision constitutes the fact whether an event is enabled or not. However, we also enable MC/DC to be applied in other contexts, e.g., to analyse invariants; in that setting a decision is whether an invariant is true or false.		A decision constitutes the fact whether an event is enabled or not. However, we also enable MC/DC to be applied in other contexts, e.g., to analyse invariants; in that setting a decision is whether an invariant is true or false.

Michael Leuschel: /* Event Coverage */

2015-09-02T06:42:33Z

Event Coverage

← Older revision		Revision as of 06:42, 2 September 2015
Line 6:		Line 6:


	== Event Coverage ==		== Operation/Event Coverage ==

	[TO DO]		[TO DO]

Michael Leuschel at 06:41, 2 September 2015

2015-09-02T06:41:57Z

← Older revision		Revision as of 06:41, 2 September 2015
Line 1:		Line 1:
	ProB provides various ways to analyse the coverage of the state space of a model		ProB provides various ways to analyse the coverage of the state space of a model.
			In ProB Tcl/Tk these features reside in the Coverage submenu of the Analyse menu:


			[[file:CoverageMenu.png\|center\|\|300px]]


	== Event Coverage ==		== Event Coverage ==
Line 17:		Line 22:
	* for the coverage for the event guards. Here it is expected that every event can be enabled or disabled.		* for the coverage for the event guards. Here it is expected that every event can be enabled or disabled.

	The algorithm is parametrised by an optional depth bound: if the depth bound is reached, then all sub-predicates are considered to be atomic decisions.		The algorithm is parametrised by an optional depth bound (called level in the coverage menu of ProB Tcl/Tk): if the depth bound is reached, then all sub-predicates are considered to be atomic decisions.
	The analysis can be used to measure the coverage of tests, but can also be used after an exhaustive model check to detect vacuous guards and vacuous invariants.		The analysis can be used to measure the coverage of tests, but can also be used after an exhaustive model check to detect vacuous guards and vacuous invariants.

Michael Leuschel: /* MC/DC Coverage */

2015-09-02T06:39:12Z

MC/DC Coverage

← Older revision		Revision as of 06:39, 2 September 2015
Line 23:		Line 23:
	Below is a screenshot of part of the output for an early version of the ABZ landing gear case study. It shows that parts of the invariant inv13 <tt>not(C0step = 0 & (gearstate = retracting & doorstate /= locked_open & handle = UP))</tt> cannot be set independently to false. This highlights a redundancy in the invariant; indeed the simpler to understand (but stronger) invariant <tt>not(gearstate = retracting & doorstate /= locked_open)</tt> holds.		Below is a screenshot of part of the output for an early version of the ABZ landing gear case study. It shows that parts of the invariant inv13 <tt>not(C0step = 0 & (gearstate = retracting & doorstate /= locked_open & handle = UP))</tt> cannot be set independently to false. This highlights a redundancy in the invariant; indeed the simpler to understand (but stronger) invariant <tt>not(gearstate = retracting & doorstate /= locked_open)</tt> holds.

	[[file:MCDC_Coverage_ABZ.png\|center\|\|~~400px~~]]		[[file:MCDC_Coverage_ABZ.png\|center\|\|700px]]

Michael Leuschel at 06:36, 2 September 2015

2015-09-02T06:36:13Z

← Older revision		Revision as of 06:36, 2 September 2015
Line 22:		Line 22:
	The MC/DC analysis has been integrated into ProB and has been successfully applied to various case studies.		The MC/DC analysis has been integrated into ProB and has been successfully applied to various case studies.
	Below is a screenshot of part of the output for an early version of the ABZ landing gear case study. It shows that parts of the invariant inv13 <tt>not(C0step = 0 & (gearstate = retracting & doorstate /= locked_open & handle = UP))</tt> cannot be set independently to false. This highlights a redundancy in the invariant; indeed the simpler to understand (but stronger) invariant <tt>not(gearstate = retracting & doorstate /= locked_open)</tt> holds.		Below is a screenshot of part of the output for an early version of the ABZ landing gear case study. It shows that parts of the invariant inv13 <tt>not(C0step = 0 & (gearstate = retracting & doorstate /= locked_open & handle = UP))</tt> cannot be set independently to false. This highlights a redundancy in the invariant; indeed the simpler to understand (but stronger) invariant <tt>not(gearstate = retracting & doorstate /= locked_open)</tt> holds.

			[[file:MCDC_Coverage_ABZ.png\|center\|\|400px]]

Michael Leuschel: Created page with 'ProB provides various ways to analyse the coverage of the state space of a model == Event Coverage == [TO DO] == MC/DC Coverage == MC/DC (Modified Condition/Decision Coverage…'

2015-09-02T06:35:05Z

Created page with 'ProB provides various ways to analyse the coverage of the state space of a model == Event Coverage == [TO DO] == MC/DC Coverage == MC/DC (Modified Condition/Decision Coverage…'

New page

ProB provides various ways to analyse the coverage of the state space of a model

== Event Coverage ==

[TO DO]

== MC/DC Coverage ==

MC/DC (Modified Condition/Decision Coverage) is a coverage criterion which is used in avionics. One core idea is ensure that for every condition in our code or model we generate at least one test where the condition independently plays an observable role in the outcome of a decision. In other words, if the condition were to be true rather than false (or vice versa) the decision would be changed. In still other words, we are trying to find an execution context where the result of the particular condition under test is crucial for the observable outcome.

In the context of B and Event-B, one question is what constitutes a condition and what constitutes a decision. In WP4 we view a condition to be an atomic predicate (e.g., x>y) not involving logical connectives (<tt>&</tt>, <tt>or</tt>, </tt>not</tt>, <tt>=></tt>, ⇔). There is, however, the possibility of treating a bigger predicate as atomic (e.g., an entire guard of an event). The reason for this is to provide better feedback to the user and to reduce the number of coverage criteria if desired. At the moment, we also consider a universally or existentially quantified formula to be a condition.
A decision constitutes the fact whether an event is enabled or not. However, we also enable MC/DC to be applied in other contexts, e.g., to analyse invariants; in that setting a decision is whether an invariant is true or false.

We have implemented a MC/DC coverage analysis which examines all visited states and computes the MC/DC coverage for a series of predicates under consideration.
Currently MC/DC coverage is used in two ways:
* for the coverage for the invariants, where the invariant is expected to be true (i.e., the analysis does not expect to find states where the invariant is false)
* for the coverage for the event guards. Here it is expected that every event can be enabled or disabled.

The algorithm is parametrised by an optional depth bound: if the depth bound is reached, then all sub-predicates are considered to be atomic decisions.
The analysis can be used to measure the coverage of tests, but can also be used after an exhaustive model check to detect vacuous guards and vacuous invariants.

The MC/DC analysis has been integrated into ProB and has been successfully applied to various case studies.
Below is a screenshot of part of the output for an early version of the ABZ landing gear case study. It shows that parts of the invariant inv13 <tt>not(C0step = 0 & (gearstate = retracting & doorstate /= locked_open & handle = UP))</tt> cannot be set independently to false. This highlights a redundancy in the invariant; indeed the simpler to understand (but stronger) invariant <tt>not(gearstate = retracting & doorstate /= locked_open)</tt> holds.