User:Nicolas/Collections/ADVANCE D3.4 Model Checking - Revision history

imported>Nicolas: /* LTL Fairness */ LTL^[e] -> LTL^[e]

2014-11-25T10:31:48Z

LTL Fairness: LTL^[e] -> LTL<sup>[e]</sup>

← Older revision		Revision as of 10:31, 25 November 2014
Line 15:		Line 15:
	==== LTL Fairness ====		==== LTL Fairness ====

	ProB provides support for checking temporal properties expressed by means of LTL (Linear Temporal Logic) or CTL (Computation Tree Logic).<ref name="LTLpaper">D. Plagge and M. Leuschel: ''Seven at one stroke: LTL model checking for High-level Specifications in B, Z, CSP, and more''. STTT, 12(1): 9-21, Feb 2010</ref> In ProB linear temporal properties can be expressed by an extended version of LTL, denoted as LTL^[e], which additionally enables the user to set propositions on transitions. Writing propositions on transitions is allowed by using the constructs `e(...)` and `[...]`. (For more information on the syntax and semantics of LTL<sup>[e]</sup> consult <ref name="LTL">ProB User Manual: LTL Model Checking, http://www.stups.uni-duesseldorf.de/ProB/index.php5/LTL_Model_Checking</ref>.)		ProB provides support for checking temporal properties expressed by means of LTL (Linear Temporal Logic) or CTL (Computation Tree Logic).<ref name="LTLpaper">D. Plagge and M. Leuschel: ''Seven at one stroke: LTL model checking for High-level Specifications in B, Z, CSP, and more''. STTT, 12(1): 9-21, Feb 2010</ref> In ProB linear temporal properties can be expressed by an extended version of LTL, denoted as LTL<sup>[e]</sup>, which additionally enables the user to set propositions on transitions. Writing propositions on transitions is allowed by using the constructs `e(...)` and `[...]`. (For more information on the syntax and semantics of LTL<sup>[e]</sup> consult <ref name="LTL">ProB User Manual: LTL Model Checking, http://www.stups.uni-duesseldorf.de/ProB/index.php5/LTL_Model_Checking</ref>.)

	Fairness is a notion where the search for counterexamples is restricted to paths that do not ignore infinitely the execution of a set of enabled actions imposed by the user as fair constraints. One possibility to set fairness constraints in ProB is to encode them in the LTL<sup>[e]</sup> formula intended to be checked. For example, for a given LTL<sup>[e]</sup> formula "f" a set of weak fairness conditions {e1,…,en} (where e1,...,en are some events) can be given as follows:		Fairness is a notion where the search for counterexamples is restricted to paths that do not ignore infinitely the execution of a set of enabled actions imposed by the user as fair constraints. One possibility to set fairness constraints in ProB is to encode them in the LTL<sup>[e]</sup> formula intended to be checked. For example, for a given LTL<sup>[e]</sup> formula "f" a set of weak fairness conditions {e1,…,en} (where e1,...,en are some events) can be given as follows:

imported>Leuschel: /* Theory Support */

2014-11-24T10:52:26Z

Theory Support

← Older revision		Revision as of 10:52, 24 November 2014
Line 86:		Line 86:
	We ensured that the Disprover also works with theories.		We ensured that the Disprover also works with theories.
	We have also improved the constraint propagation of the ProB kernel for records and freetypes, which are used to represent Event-B inductive datatypes.		We have also improved the constraint propagation of the ProB kernel for records and freetypes, which are used to represent Event-B inductive datatypes.
	(As a side note, this feature is also being used for validating VDM specifications using ProB within the [http://overturetool.org Ouverture] tool <ref>~~Interpreting Implicit VDM Specifications using ProB.~~ Lausdahl, Kenneth; Ishikawa, Hiroshi; Larsen, Peter Gorm.2014. Abstract from 12th Overture Workshop on VDM, Newcastle, United Kingdom. http://wiki.overturetool.org/index.php/12th_Overture_Workshop.</ref>. Ouverture is the subject of ongoing and past EU projects, e.g., Destecs or ~~Compass~~ http://www.compass-research.eu.).		(As a side note, this feature is also being used for validating VDM specifications using ProB within the [http://overturetool.org Ouverture] tool <ref>Lausdahl, Kenneth; Ishikawa, Hiroshi; Larsen, Peter Gorm. Interpreting Implicit VDM Specifications using ProB. 2014. Abstract from 12th Overture Workshop on VDM, Newcastle, United Kingdom. http://wiki.overturetool.org/index.php/12th_Overture_Workshop.</ref>. Ouverture is the subject of ongoing and past EU projects, e.g., [http://destecs.org Destecs] or [http://www.compass-research.eu Compass].).
	Finally, the treatment of recursive functions within the ProB kernel has been improved, also in light of dealing with recursive operators of Event-B Theories.		Finally, the treatment of recursive functions within the ProB kernel has been improved, also in light of dealing with recursive operators of Event-B Theories.
	More details can be found in deliverable D4.4 (ProB constraint solving kernel).		More details can be found in deliverable D4.4 (ProB constraint solving kernel).

imported>Leuschel: /* Theory Support */

2014-11-24T10:50:56Z

Theory Support

← Older revision		Revision as of 10:50, 24 November 2014
Line 86:		Line 86:
	We ensured that the Disprover also works with theories.		We ensured that the Disprover also works with theories.
	We have also improved the constraint propagation of the ProB kernel for records and freetypes, which are used to represent Event-B inductive datatypes.		We have also improved the constraint propagation of the ProB kernel for records and freetypes, which are used to represent Event-B inductive datatypes.
	(As a side note, this feature is also being used ~~by another EU project to use ProB~~ for validating VDM specifications within the Ouverture tool).		(As a side note, this feature is also being used for validating VDM specifications using ProB within the [http://overturetool.org Ouverture] tool <ref>Interpreting Implicit VDM Specifications using ProB. Lausdahl, Kenneth; Ishikawa, Hiroshi; Larsen, Peter Gorm.2014. Abstract from 12th Overture Workshop on VDM, Newcastle, United Kingdom. http://wiki.overturetool.org/index.php/12th_Overture_Workshop.</ref>. Ouverture is the subject of ongoing and past EU projects, e.g., Destecs or Compass http://www.compass-research.eu.).
	Finally, the treatment of recursive functions within the ProB kernel has been improved, also in light of dealing with recursive operators of Event-B Theories.		Finally, the treatment of recursive functions within the ProB kernel has been improved, also in light of dealing with recursive operators of Event-B Theories.
	More details can be found in deliverable D4.4 (ProB constraint solving kernel).		More details can be found in deliverable D4.4 (ProB constraint solving kernel).

imported>Leuschel: /* Theory Support */

2014-11-24T10:42:15Z

Theory Support

← Older revision		Revision as of 10:42, 24 November 2014
Line 84:		Line 84:

	Theory Support was relevant for a variety of case studies, and is relevant for simulation, model checking and proving.		Theory Support was relevant for a variety of case studies, and is relevant for simulation, model checking and proving.
	We ensured that the Disprover also works with theories		We ensured that the Disprover also works with theories.
	We have also improved the constraint propagation of the ProB kernel for records and freetypes, which are used to represent Event-B inductive datatypes.		We have also improved the constraint propagation of the ProB kernel for records and freetypes, which are used to represent Event-B inductive datatypes.
	(As a side note, this feature is also being used by another EU project to use ProB for validating VDM specifications within the Ouverture tool).		(As a side note, this feature is also being used by another EU project to use ProB for validating VDM specifications within the Ouverture tool).

imported>Ladenberger: /* New LTL Patterns */

2014-11-21T15:51:46Z

New LTL Patterns

← Older revision		Revision as of 15:51, 21 November 2014
Line 75:		Line 75:
	* controller(e1,e2,…,ek), where e1,e2,...,ek with k>0 are events. Used to check that exactly one of the events e1,e2,...,ek is enabled in a state.		* controller(e1,e2,…,ek), where e1,e2,...,ek with k>0 are events. Used to check that exactly one of the events e1,e2,...,ek is enabled in a state.

	Referring to the landing gear case study from <ref name="Landing Gear""> </ref>, one important issue in the process of validation of the model was to guarantee that the controller behaves in a determinisitc way. In the corresponding model the behavior of the controller is divided into several events: con_stop_stimulate_extend_gear_valve, con_stimulate_extend_gear_valve, con_stop_stimulate_retract_gear_valve, etc. The deterministic behavior of the controller could, for example, be tested by using new LTL pattern `deterministic(e1,e2,…,ek)` within an LTL<sup>[e]</sup> formula:		Referring to the landing gear case study from <ref name="Landing Gear"> </ref>, one important issue in the process of validation of the model was to guarantee that the controller behaves in a determinisitc way. In the corresponding model the behavior of the controller is divided into several events: con_stop_stimulate_extend_gear_valve, con_stimulate_extend_gear_valve, con_stop_stimulate_retract_gear_valve, etc. The deterministic behavior of the controller could, for example, be tested by using new LTL pattern `deterministic(e1,e2,…,ek)` within an LTL<sup>[e]</sup> formula:

	G deterministic(con_stop_stimulate_extend_gear_valve,con_stimulate_extend_gear_valve,con_stop_stimulate_retract_gear_valve,...)		G deterministic(con_stop_stimulate_extend_gear_valve,con_stimulate_extend_gear_valve,con_stop_stimulate_retract_gear_valve,...)

imported>Ladenberger: /* B to TLA+ */

2014-11-21T15:35:00Z

B to TLA+

← Older revision		Revision as of 15:35, 21 November 2014
Line 104:		Line 104:
	=== B to TLA+ ===		=== B to TLA+ ===

	We are interested in validating the correctness of our translation from B to TLA+.		We developed a translation from B to TLA+ to verify B specifications with TLC. TLC is an explicit state model checker for TLA+ providing a parallel and a distributed mode. It is particularly good for lower level specifications, where it can be substantially faster than ProB's own model checker.
	Hence, we have conducted extensive tests to validate our approach.
	For example, we use a range of models encoding mathematical laws to stress test our translation.		Moreover, we are interested in validating the correctness of our translation from B to TLA+. Hence, we have conducted extensive tests to validate our approach. For example, we use a range of models encoding mathematical laws to stress test our translation. These have proven to be very useful for detecting bugs in our translation and libraries. In addition, we have uncovered a bug in the model checker TLC. Moreover, we use a wide variety of benchmarks, checking that ProB and TLC produce the same result and generate the same number of states
	These have proven to be very useful for detecting bugs in our translation and libraries.
	In addition, we have uncovered a bug in the model checker TLC.
	Moreover, we use a wide variety of benchmarks, checking that ProB and TLC produce the same result and generate the same number of states.

	The current version of our translator covers almost all operators of a abstract B machine.		The current version of our translator covers almost all operators of a abstract B machine.

imported>Ladenberger at 15:34, 21 November 2014

2014-11-21T15:34:36Z

← Older revision		Revision as of 15:34, 21 November 2014
Line 7:		Line 7:
	== Motivations / Decisions ==		== Motivations / Decisions ==

	== Linear Temporal Logic ==		=== Linear Temporal Logic ===

	LTL is a specification language used for specifying temporal properties of a system. A possible requirement that could refer to WP1 may be, for example, ''once a block is reserved, it will eventually be occupied''. The requirement could be easily written as an LTL formula using the temporal operators `G` (always) and `F` (eventually):		LTL is a specification language used for specifying temporal properties of a system. A possible requirement that could refer to WP1 may be, for example, ''once a block is reserved, it will eventually be occupied''. The requirement could be easily written as an LTL formula using the temporal operators `G` (always) and `F` (eventually):
Line 13:		Line 13:
	`G ({reserved(B) = TRUE} => F {occupied(B) = TRUE})`, where ''B'' is a block of some track segment in the railway network and the expressions inside the curly brackets `{...}` are B predicates.		`G ({reserved(B) = TRUE} => F {occupied(B) = TRUE})`, where ''B'' is a block of some track segment in the railway network and the expressions inside the curly brackets `{...}` are B predicates.

	=== LTL Fairness ===		==== LTL Fairness ====

	ProB provides support for checking temporal properties expressed by means of LTL (Linear Temporal Logic) or CTL (Computation Tree Logic).<ref name="LTLpaper">D. Plagge and M. Leuschel: ''Seven at one stroke: LTL model checking for High-level Specifications in B, Z, CSP, and more''. STTT, 12(1): 9-21, Feb 2010</ref> In ProB linear temporal properties can be expressed by an extended version of LTL, denoted as LTL^[e], which additionally enables the user to set propositions on transitions. Writing propositions on transitions is allowed by using the constructs `e(...)` and `[...]`. (For more information on the syntax and semantics of LTL<sup>[e]</sup> consult <ref name="LTL">ProB User Manual: LTL Model Checking, http://www.stups.uni-duesseldorf.de/ProB/index.php5/LTL_Model_Checking</ref>.)		ProB provides support for checking temporal properties expressed by means of LTL (Linear Temporal Logic) or CTL (Computation Tree Logic).<ref name="LTLpaper">D. Plagge and M. Leuschel: ''Seven at one stroke: LTL model checking for High-level Specifications in B, Z, CSP, and more''. STTT, 12(1): 9-21, Feb 2010</ref> In ProB linear temporal properties can be expressed by an extended version of LTL, denoted as LTL^[e], which additionally enables the user to set propositions on transitions. Writing propositions on transitions is allowed by using the constructs `e(...)` and `[...]`. (For more information on the syntax and semantics of LTL<sup>[e]</sup> consult <ref name="LTL">ProB User Manual: LTL Model Checking, http://www.stups.uni-duesseldorf.de/ProB/index.php5/LTL_Model_Checking</ref>.)
Line 40:		Line 40:
	More information on setting fairness to LTL formulas and the LTL Model Checker is available on the ProB User Manual website <ref name="LTL"> </ref>.		More information on setting fairness to LTL formulas and the LTL Model Checker is available on the ProB User Manual website <ref name="LTL"> </ref>.

	==== Use Case ====		===== Use Case =====

	Consider an Event-B model formalizing an algorithm for mutual exclusion with semaphores for two concurrent processes <math>P_1</math> and <math>P_2</math>. Each process has been simplified to perform three types of events: ''request'' (for entering in the critical section), ''enter'' (entering the critical section), and ''release'' (exiting the critical section). (For more information on the algorithm and the design of the model see <ref>C.Baier and J.-P. Katoen. “Principles of Model Checking”, The MIT Press, 2008, pages 43-45.</ref>).		Consider an Event-B model formalizing an algorithm for mutual exclusion with semaphores for two concurrent processes <math>P_1</math> and <math>P_2</math>. Each process has been simplified to perform three types of events: ''request'' (for entering in the critical section), ''enter'' (entering the critical section), and ''release'' (exiting the critical section). (For more information on the algorithm and the design of the model see <ref>C.Baier and J.-P. Katoen. “Principles of Model Checking”, The MIT Press, 2008, pages 43-45.</ref>).

imported>Ladenberger: /* LTL Fairness */

2014-11-21T15:32:57Z

LTL Fairness

Show changes

imported>Nicolas: remove end of line inside ref, that causes bad display when translated to pdf

2014-11-12T11:48:04Z

remove end of line inside ref, that causes bad display when translated to pdf

← Older revision		Revision as of 11:48, 12 November 2014
Line 30:		Line 30:
	** `&` and `or`: conjunction and disjunction		** `&` and `or`: conjunction and disjunction

	More information on setting fairness to LTL formulas and the LTL Model Checker is available on the ProB User Manual website <ref name="LTL">ProB User Manual: LTL Model Checking,		More information on setting fairness to LTL formulas and the LTL Model Checker is available on the ProB User Manual website <ref name="LTL">ProB User Manual: LTL Model Checking, http://www.stups.uni-duesseldorf.de/ProB/index.php5/LTL_Model_Checking</ref>.
	http://www.stups.uni-duesseldorf.de/ProB/index.php5/LTL_Model_Checking</ref>.

	==== Use Case ====		==== Use Case ====

imported>Leuschel: /* Theory Support */

2014-11-07T14:07:56Z

Theory Support

← Older revision		Revision as of 14:07, 7 November 2014
Line 75:		Line 75:
	(As a side note, this feature is also being used by another EU project to use ProB for validating VDM specifications within the Ouverture tool).		(As a side note, this feature is also being used by another EU project to use ProB for validating VDM specifications within the Ouverture tool).
	Finally, the treatment of recursive functions within the ProB kernel has been improved, also in light of dealing with recursive operators of Event-B Theories.		Finally, the treatment of recursive functions within the ProB kernel has been improved, also in light of dealing with recursive operators of Event-B Theories.
			More details can be found in deliverable D4.4 (ProB constraint solving kernel).

	=== Physical Units ===		=== Physical Units ===

User:Nicolas/Collections/ADVANCE D3.4 Model Checking - Revision history

imported>Nicolas: /* LTL Fairness */ LTL^[e] -> LTL[e]

imported>Leuschel: /* Theory Support */

imported>Leuschel: /* Theory Support */

imported>Leuschel: /* Theory Support */

imported>Ladenberger: /* New LTL Patterns */

imported>Ladenberger: /* B to TLA+ */

imported>Ladenberger at 15:34, 21 November 2014

imported>Ladenberger: /* LTL Fairness */

imported>Nicolas: remove end of line inside ref, that causes bad display when translated to pdf

imported>Leuschel: /* Theory Support */

imported>Nicolas: /* LTL Fairness */ LTL^[e] -> LTL^[e]