Constraint Based Checking - Revision history

Michael Leuschel at 09:58, 10 March 2015

2015-03-10T09:58:25Z

← Older revision		Revision as of 09:58, 10 March 2015
Line 2:		Line 2:

	ProB also offers an alternative checking method, inspired by the Alloy		ProB also offers an alternative checking method, inspired by the Alloy
	<ref>D. Jackson: Alloy: A lightweight object modeling notation. ACM Transactions Software Engineering and Methodology (TOSEM), 11(2):256–290, 2002.</ref> analyser. In this mode of operation, ProB does not explore the reachable states starting from the initial state(s), but checks whether applying a single operation can result in a property violation (invariant and assertion) independently of the particular initialization of the B machine. This is done by symbolic constraint solving, and we call this approach constraint based checking (another sensible name would be model finding).		<ref>D. Jackson: Alloy: A lightweight object modeling notation. ACM Transactions Software Engineering and Methodology (TOSEM), 11(2):256–290, 2002.</ref> analyser. In this mode of operation, ProB does not explore the reachable states starting from the initial state(s), but checks whether applying a <b>single</b> operation can result in a property violation (invariant and assertion) independently of the particular initialization of the B machine. This is done by symbolic constraint solving, and we call this approach constraint based checking (another sensible name would be model finding).

	More details and examples can be found in the [[Tutorial_Model_Checking,_Proof_and_CBC\|tutorial page on model checking, proof and CBC]].		More details and examples can be found in the [[Tutorial_Model_Checking,_Proof_and_CBC\|tutorial page on model checking, proof and CBC]].
Line 9:		Line 9:
	=Difference between Constraint Based Checking and Model Checking=		=Difference between Constraint Based Checking and Model Checking=

	Model checking tries to find a sequence of operations that, starting from an initial state, leads to a state which violates a property. Constraint based checking tries to find a state of the machine that satisfies the property but where we can apply a single operation to reach a state that violates this property. If the constraint based checker finds a counter-example, this indicates that the B specification may contain a problem. The sequence of operations discovered by the constraint based checker leads from a valid state to a property violation, meaning that the B machine may have to be corrected. The valid state is not necessarily reachable from a valid initial state. This situation further indicates that it will be impossible to prove the machine using the B proof rules.		[[Consistency_Checking\|Model checking]] tries to find a sequence of operations that, starting from an initial state, leads to a state which violates a property. Constraint based checking tries to find a state of the machine that satisfies the property but where we can apply a single operation to reach a state that violates this property. If the constraint based checker finds a counter-example, this indicates that the B specification may contain a problem. The sequence of operations discovered by the constraint based checker leads from a valid state to a property violation, meaning that the B machine may have to be corrected. The valid state is not necessarily reachable from a valid initial state. This situation further indicates that it will be impossible to prove the machine using the B proof rules.
	In other words, the constraint-based checker verifies that the invariant is <b>inductive</b>.		In other words, the constraint-based checker verifies that the invariant is <b>inductive</b>.

Michael Leuschel at 09:56, 10 March 2015

2015-03-10T09:56:31Z

← Older revision		Revision as of 09:56, 10 March 2015
Line 1:		Line 1:
	[[Category:User Manual]]		[[Category:User Manual]]
	~~{{Revision}}~~
	ProB also offers an alternative checking method, inspired by the Alloy		ProB also offers an alternative checking method, inspired by the Alloy
	<ref>D. Jackson: Alloy: A lightweight object modeling notation. ACM Transactions Software Engineering and Methodology (TOSEM), 11(2):256–290, 2002.</ref> analyser. In this mode of operation, ProB does not explore the reachable states starting from the initial state(s), but checks whether applying a single operation can result in a property violation (invariant and assertion) independently of the particular initialization of the B machine. This is done by symbolic constraint solving, and we call this approach constraint based checking (another sensible name would be model finding).		<ref>D. Jackson: Alloy: A lightweight object modeling notation. ACM Transactions Software Engineering and Methodology (TOSEM), 11(2):256–290, 2002.</ref> analyser. In this mode of operation, ProB does not explore the reachable states starting from the initial state(s), but checks whether applying a single operation can result in a property violation (invariant and assertion) independently of the particular initialization of the B machine. This is done by symbolic constraint solving, and we call this approach constraint based checking (another sensible name would be model finding).
Line 10:		Line 10:

	Model checking tries to find a sequence of operations that, starting from an initial state, leads to a state which violates a property. Constraint based checking tries to find a state of the machine that satisfies the property but where we can apply a single operation to reach a state that violates this property. If the constraint based checker finds a counter-example, this indicates that the B specification may contain a problem. The sequence of operations discovered by the constraint based checker leads from a valid state to a property violation, meaning that the B machine may have to be corrected. The valid state is not necessarily reachable from a valid initial state. This situation further indicates that it will be impossible to prove the machine using the B proof rules.		Model checking tries to find a sequence of operations that, starting from an initial state, leads to a state which violates a property. Constraint based checking tries to find a state of the machine that satisfies the property but where we can apply a single operation to reach a state that violates this property. If the constraint based checker finds a counter-example, this indicates that the B specification may contain a problem. The sequence of operations discovered by the constraint based checker leads from a valid state to a property violation, meaning that the B machine may have to be corrected. The valid state is not necessarily reachable from a valid initial state. This situation further indicates that it will be impossible to prove the machine using the B proof rules.
			In other words, the constraint-based checker verifies that the invariant is <b>inductive</b>.

	A comparison between all [[ProB_Validation_Methods\|ProB validation methods can be found on a separate manual page]].		A comparison between all [[ProB_Validation_Methods\|ProB validation methods can be found on a separate manual page]].

Michael Leuschel: /* Difference between Constraint Based Checking and Model Checking */

2015-01-16T09:02:11Z

Difference between Constraint Based Checking and Model Checking

← Older revision		Revision as of 09:02, 16 January 2015
Line 10:		Line 10:

	Model checking tries to find a sequence of operations that, starting from an initial state, leads to a state which violates a property. Constraint based checking tries to find a state of the machine that satisfies the property but where we can apply a single operation to reach a state that violates this property. If the constraint based checker finds a counter-example, this indicates that the B specification may contain a problem. The sequence of operations discovered by the constraint based checker leads from a valid state to a property violation, meaning that the B machine may have to be corrected. The valid state is not necessarily reachable from a valid initial state. This situation further indicates that it will be impossible to prove the machine using the B proof rules.		Model checking tries to find a sequence of operations that, starting from an initial state, leads to a state which violates a property. Constraint based checking tries to find a state of the machine that satisfies the property but where we can apply a single operation to reach a state that violates this property. If the constraint based checker finds a counter-example, this indicates that the B specification may contain a problem. The sequence of operations discovered by the constraint based checker leads from a valid state to a property violation, meaning that the B machine may have to be corrected. The valid state is not necessarily reachable from a valid initial state. This situation further indicates that it will be impossible to prove the machine using the B proof rules.

			A comparison between all [[ProB_Validation_Methods\|ProB validation methods can be found on a separate manual page]].

	=Commands of the Constraint Based Checker =		=Commands of the Constraint Based Checker =

Michael Leuschel: /* Commands of the Constraint Based Checker */

2015-01-16T07:10:52Z

Commands of the Constraint Based Checker

← Older revision		Revision as of 07:10, 16 January 2015
Line 17:		Line 17:

	Within the [[Using_the_Command-Line_Version_of_ProB\|command-line version of ProB]], there are also several commands available:		Within the [[Using_the_Command-Line_Version_of_ProB\|command-line version of ProB]], there are also several commands available:
	* [[Using_the_Command-Line_Version_of_ProB#-cbc_.3COPNAME.3E\|cbc OP]] to check whether an operation preserves the invariant		* [[Using_the_Command-Line_Version_of_ProB#-cbc_.3COPNAME.3E\|cbc <OP>]] to check whether an operation preserves the invariant
	* [[Using_the_Command-Line_Version_of_ProB#-cbc_deadlock\|cbc_deadlock]] to check whether the invariant implies that no deadlock is possible		* [[Using_the_Command-Line_Version_of_ProB#-cbc_deadlock\|cbc_deadlock]] to check whether the invariant implies that no deadlock is possible
	* [[Using_the_Command-Line_Version_of_ProB#-cbc_assertions\|cbc_assertions]] to check whether the static assertions (on constants) are implied by the axioms/properties.		* [[Using_the_Command-Line_Version_of_ProB#-cbc_assertions\|cbc_assertions]] to check whether the static assertions (on constants) are implied by the axioms/properties.

	The following command is related to the above:		The following command is related to the above:
	* [[Using_the_Command-Line_Version_of_ProB#-cbc_sequence_.3CSEQ.3E\|cbc_sequence]] to find a sequence of operations using the constraint solver		* [[Using_the_Command-Line_Version_of_ProB#-cbc_sequence_.3CSEQ.3E\|cbc_sequence <SEQ>]] to find a sequence of operations using the constraint solver

	=References=		=References=
	<references />		<references />

Michael Leuschel: /* Commands of the Constraint Based Checker */

2015-01-16T07:09:50Z

Commands of the Constraint Based Checker

← Older revision		Revision as of 07:09, 16 January 2015
Line 22:		Line 22:

	The following command is related to the above:		The following command is related to the above:
	* [[Using_the_Command-Line_Version_of_ProB#-~~cbc_sequence~~\|cbc_sequence]] to find a sequence of operations using the constraint solver		* [[Using_the_Command-Line_Version_of_ProB#-cbc_sequence_.3CSEQ.3E\|cbc_sequence]] to find a sequence of operations using the constraint solver

	=References=		=References=
	<references />		<references />

Michael Leuschel: /* Commands of the Constraint Based Checker */

2015-01-16T07:05:14Z

Commands of the Constraint Based Checker

← Older revision		Revision as of 07:05, 16 January 2015
Line 17:		Line 17:

	Within the [[Using_the_Command-Line_Version_of_ProB\|command-line version of ProB]], there are also several commands available:		Within the [[Using_the_Command-Line_Version_of_ProB\|command-line version of ProB]], there are also several commands available:
	* [[Using_the_Command-Line_Version_of_ProB#-cbc_.3COPNAME.3E\|cbc OP]		* [[Using_the_Command-Line_Version_of_ProB#-cbc_.3COPNAME.3E\|cbc OP]] to check whether an operation preserves the invariant
	* [[Using_the_Command-Line_Version_of_ProB#-cbc_deadlock\|cbc_deadlock]]		* [[Using_the_Command-Line_Version_of_ProB#-cbc_deadlock\|cbc_deadlock]] to check whether the invariant implies that no deadlock is possible
	* [[Using_the_Command-Line_Version_of_ProB#-cbc_assertions\|cbc_assertions]]		* [[Using_the_Command-Line_Version_of_ProB#-cbc_assertions\|cbc_assertions]] to check whether the static assertions (on constants) are implied by the axioms/properties.
	* [[Using_the_Command-Line_Version_of_ProB#-cbc_sequence\|cbc_sequence]]
			The following command is related to the above:
			* [[Using_the_Command-Line_Version_of_ProB#-cbc_sequence\|cbc_sequence]] to find a sequence of operations using the constraint solver

	=References=		=References=
	<references />		<references />

Michael Leuschel at 07:03, 16 January 2015

2015-01-16T07:03:14Z

← Older revision		Revision as of 07:03, 16 January 2015
Line 3:		Line 3:
	ProB also offers an alternative checking method, inspired by the Alloy		ProB also offers an alternative checking method, inspired by the Alloy
	<ref>D. Jackson: Alloy: A lightweight object modeling notation. ACM Transactions Software Engineering and Methodology (TOSEM), 11(2):256–290, 2002.</ref> analyser. In this mode of operation, ProB does not explore the reachable states starting from the initial state(s), but checks whether applying a single operation can result in a property violation (invariant and assertion) independently of the particular initialization of the B machine. This is done by symbolic constraint solving, and we call this approach constraint based checking (another sensible name would be model finding).		<ref>D. Jackson: Alloy: A lightweight object modeling notation. ACM Transactions Software Engineering and Methodology (TOSEM), 11(2):256–290, 2002.</ref> analyser. In this mode of operation, ProB does not explore the reachable states starting from the initial state(s), but checks whether applying a single operation can result in a property violation (invariant and assertion) independently of the particular initialization of the B machine. This is done by symbolic constraint solving, and we call this approach constraint based checking (another sensible name would be model finding).

			More details and examples can be found in the [[Tutorial_Model_Checking,_Proof_and_CBC\|tutorial page on model checking, proof and CBC]].


Line 13:		Line 15:

	The "Constraint Search for Assertion Violations" command executes the constraint based checking looking for assertion violations, while the command "Constraint Search for Abort Conditions" executes it looking for abort conditions.		The "Constraint Search for Assertion Violations" command executes the constraint based checking looking for assertion violations, while the command "Constraint Search for Abort Conditions" executes it looking for abort conditions.

			Within the [[Using_the_Command-Line_Version_of_ProB\|command-line version of ProB]], there are also several commands available:
			* [[Using_the_Command-Line_Version_of_ProB#-cbc_.3COPNAME.3E\|cbc OP]
			* [[Using_the_Command-Line_Version_of_ProB#-cbc_deadlock\|cbc_deadlock]]
			* [[Using_the_Command-Line_Version_of_ProB#-cbc_assertions\|cbc_assertions]]
			* [[Using_the_Command-Line_Version_of_ProB#-cbc_sequence\|cbc_sequence]]

	=References=		=References=
	<references />		<references />

Michael Leuschel at 12:59, 3 June 2014

2014-06-03T12:59:47Z

← Older revision		Revision as of 12:59, 3 June 2014
Line 4:		Line 4:
	<ref>D. Jackson: Alloy: A lightweight object modeling notation. ACM Transactions Software Engineering and Methodology (TOSEM), 11(2):256–290, 2002.</ref> analyser. In this mode of operation, ProB does not explore the reachable states starting from the initial state(s), but checks whether applying a single operation can result in a property violation (invariant and assertion) independently of the particular initialization of the B machine. This is done by symbolic constraint solving, and we call this approach constraint based checking (another sensible name would be model finding).		<ref>D. Jackson: Alloy: A lightweight object modeling notation. ACM Transactions Software Engineering and Methodology (TOSEM), 11(2):256–290, 2002.</ref> analyser. In this mode of operation, ProB does not explore the reachable states starting from the initial state(s), but checks whether applying a single operation can result in a property violation (invariant and assertion) independently of the particular initialization of the B machine. This is done by symbolic constraint solving, and we call this approach constraint based checking (another sensible name would be model finding).

	Warning: this feature of ProB has not received the same level of attention and testing as the animation or temporal model checking. We have not had the time to put a lot of effort into this feature in the past years, so it will probably only work for simpler B machines.

	=Difference between Constraint Based Checking and Model Checking=		=Difference between Constraint Based Checking and Model Checking=

Joy Clark: " "

2011-04-18T11:48:11Z

" "

← Older revision		Revision as of 11:48, 18 April 2011
Line 2:		Line 2:
	{{Revision}}		{{Revision}}
	ProB also offers an alternative checking method, inspired by the Alloy		ProB also offers an alternative checking method, inspired by the Alloy
	<ref>D. Jackson: Alloy: A lightweight object ~~modelling~~ notation. ACM Transactions Software Engineering and Methodology (TOSEM), 11(2):256–290, 2002.</ref> analyser. In this mode of operation, ProB does not explore the reachable states starting from the initial state(s), but checks whether applying a single operation can result in a property violation (invariant and assertion) independently of the particular initialization of the B machine. This is done by symbolic constraint solving, and we call this approach constraint based checking (another sensible name would be model finding).		<ref>D. Jackson: Alloy: A lightweight object modeling notation. ACM Transactions Software Engineering and Methodology (TOSEM), 11(2):256–290, 2002.</ref> analyser. In this mode of operation, ProB does not explore the reachable states starting from the initial state(s), but checks whether applying a single operation can result in a property violation (invariant and assertion) independently of the particular initialization of the B machine. This is done by symbolic constraint solving, and we call this approach constraint based checking (another sensible name would be model finding).

	Warning: this feature of ProB has not received the same level of attention and testing as the animation or temporal model checking. We have not had the time to put a lot of effort into this feature in the past years, so it will probably only work for simpler B machines.		Warning: this feature of ProB has not received the same level of attention and testing as the animation or temporal model checking. We have not had the time to put a lot of effort into this feature in the past years, so it will probably only work for simpler B machines.
Line 11:		Line 11:
	=Commands of the Constraint Based Checker =		=Commands of the Constraint Based Checker =

	These commands are only accessible in the Normal mode of ProB (see [[General Presentation (tcl/tk)#The ProB main window\|General Presentation]]) and are in the ~~submenu~~ Verify\|Constraint Based Checking. The command Constraint Search for Invariant Violations will execute the constraint based checking described above to check for invariant violations. The process stops as soon as a counterexample has been found and then displays the counter-example in the animation panes. The command Constraint Search for Invariant Violations... enables the user to specify which particular operation leading from the valid state to the invariant violation of the B specification should be considered during the constraint based checking.		These commands are only accessible in the "Normal" mode of ProB (see [[General Presentation (tcl/tk)#The ProB main window\|General Presentation]]) and are in the sub-menu "Verify\|Constraint Based Checking". The command "Constraint Search for Invariant Violations" will execute the constraint based checking described above to check for invariant violations. The process stops as soon as a counterexample has been found and then displays the counter-example in the animation panes. The command "Constraint Search for Invariant Violations..." enables the user to specify which particular operation leading from the valid state to the invariant violation of the B specification should be considered during the constraint based checking.

	The Constraint Search for Assertion Violations command executes the constraint based checking looking for assertion violations, while the command Constraint Search for Abort Conditions executes it looking for abort conditions.		The "Constraint Search for Assertion Violations" command executes the constraint based checking looking for assertion violations, while the command "Constraint Search for Abort Conditions" executes it looking for abort conditions.

	=References=		=References=
	<references />		<references />

Joy Clark: grammatical edits, punctuation edits

2011-04-14T13:05:13Z

grammatical edits, punctuation edits

← Older revision		Revision as of 13:05, 14 April 2011
Line 2:		Line 2:
	{{Revision}}		{{Revision}}
	ProB also offers an alternative checking method, inspired by the Alloy		ProB also offers an alternative checking method, inspired by the Alloy
	<ref>D. Jackson: Alloy: A lightweight object modelling notation. ACM Transactions Software Engineering and Methodology (TOSEM), 11(2):256–290, 2002.</ref> analyser. In this mode of operation, ProB does not explore the reachable states starting from the initial state(s), but checks whether applying a single operation can result in a property violation (invariant and assertion), independently of the particular ~~initialisation~~ of the B machine. This is done by symbolic constraint solving, and we call this approach constraint based checking (another sensible name would be model finding).		<ref>D. Jackson: Alloy: A lightweight object modelling notation. ACM Transactions Software Engineering and Methodology (TOSEM), 11(2):256–290, 2002.</ref> analyser. In this mode of operation, ProB does not explore the reachable states starting from the initial state(s), but checks whether applying a single operation can result in a property violation (invariant and assertion) independently of the particular initialization of the B machine. This is done by symbolic constraint solving, and we call this approach constraint based checking (another sensible name would be model finding).

	Warning: this feature of ProB has not received the same level of attention and testing as animation or temporal model checking. We have not had the time to put a lot of effort into this feature in the past years, ~~hence~~ it will probably only work for simpler B machines.		Warning: this feature of ProB has not received the same level of attention and testing as the animation or temporal model checking. We have not had the time to put a lot of effort into this feature in the past years, so it will probably only work for simpler B machines.

	=Difference between Constraint Based Checking and Model Checking=		=Difference between Constraint Based Checking and Model Checking=

	Model checking tries to find a sequence of operations that, starting from an initial state, leads to a state which violates a property. Constraint based checking tries to find a state of the machine that satisfies the property, but where we can apply a single operation to reach a state that violates this property. If the constraint based checker finds a counter-example, this indicates that the B specification may contain a problem. The sequence of operations discovered by the constraint based checker leads from a valid state to a property violation, meaning that the B machine may have to be corrected. The valid state is not necessarily reachable from a valid initial state. This situation further indicates that it will be impossible to prove the machine using the B proof rules.		Model checking tries to find a sequence of operations that, starting from an initial state, leads to a state which violates a property. Constraint based checking tries to find a state of the machine that satisfies the property but where we can apply a single operation to reach a state that violates this property. If the constraint based checker finds a counter-example, this indicates that the B specification may contain a problem. The sequence of operations discovered by the constraint based checker leads from a valid state to a property violation, meaning that the B machine may have to be corrected. The valid state is not necessarily reachable from a valid initial state. This situation further indicates that it will be impossible to prove the machine using the B proof rules.
	=Commands of the Constraint Based Checker =		=Commands of the Constraint Based Checker =

	These commands are only accessible in the Normal mode of ProB (see [[General Presentation (tcl/tk)#The ProB main window\|General Presentation]]) and are in the submenu Verify\|Constraint Based Checking. The command Constraint Search for Invariant Violations will execute the constraint based checking described above~~, checking~~ for invariant violations. The process stops as soon as a counterexample has been found and then displays the counter-example in the animation panes. The command Constraint Search for Invariant Violations... enables the user to specify which particular operation leading from the valid state to the invariant violation of the B specification should be considered during the constraint based checking.		These commands are only accessible in the Normal mode of ProB (see [[General Presentation (tcl/tk)#The ProB main window\|General Presentation]]) and are in the submenu Verify\|Constraint Based Checking. The command Constraint Search for Invariant Violations will execute the constraint based checking described above to check for invariant violations. The process stops as soon as a counterexample has been found and then displays the counter-example in the animation panes. The command Constraint Search for Invariant Violations... enables the user to specify which particular operation leading from the valid state to the invariant violation of the B specification should be considered during the constraint based checking.

	The Constraint Search for Assertion Violations command executes the constraint based checking looking for assertion violations, while the command Constraint Search for Abort Conditions executes it looking for abort conditions.		The Constraint Search for Assertion Violations command executes the constraint based checking looking for assertion violations, while the command Constraint Search for Abort Conditions executes it looking for abort conditions.

← Older revision		Revision as of 07:05, 16 January 2015
Line 17:		Line 17:

	Within the [[Using_the_Command-Line_Version_of_ProB\|command-line version of ProB]], there are also several commands available:		Within the [[Using_the_Command-Line_Version_of_ProB\|command-line version of ProB]], there are also several commands available:
	* [[Using_the_Command-Line_Version_of_ProB#-cbc_.3COPNAME.3E\|cbc OP]		* [[Using_the_Command-Line_Version_of_ProB#-cbc_.3COPNAME.3E\|cbc OP]] to check whether an operation preserves the invariant
	* [[Using_the_Command-Line_Version_of_ProB#-cbc_deadlock\|cbc_deadlock]]		* [[Using_the_Command-Line_Version_of_ProB#-cbc_deadlock\|cbc_deadlock]] to check whether the invariant implies that no deadlock is possible
	* [[Using_the_Command-Line_Version_of_ProB#-cbc_assertions\|cbc_assertions]]		* [[Using_the_Command-Line_Version_of_ProB#-cbc_assertions\|cbc_assertions]] to check whether the static assertions (on constants) are implied by the axioms/properties.
	* [[Using_the_Command-Line_Version_of_ProB#-cbc_sequence\|cbc_sequence]]
			The following command is related to the above:
			* [[Using_the_Command-Line_Version_of_ProB#-cbc_sequence\|cbc_sequence]] to find a sequence of operations using the constraint solver

	=References=		=References=
	<references />		<references />