ADVANCE D3.3 Model Checking - Revision history

imported>Jens: /* Motivations / Decisions */

2013-09-23T10:41:48Z

Motivations / Decisions

← Older revision		Revision as of 10:41, 23 September 2013
Line 20:		Line 20:

	We developed a transcompiler from B to TLA<sup>+</sup> (Temporal Logic of Actions) to verify B specifications with TLC. TLC is an explicit state model checker for TLA<sup>+</sup> with an efficient disk-based algorithm and support for temporal formulas and fairness.Our translator is full automatic and supports a large subset of B.		We developed a transcompiler from B to TLA<sup>+</sup> (Temporal Logic of Actions) to verify B specifications with TLC. TLC is an explicit state model checker for TLA<sup>+</sup> with an efficient disk-based algorithm and support for temporal formulas and fairness.Our translator is full automatic and supports a large subset of B.
	Moreover it uses static analyses to verify the ~~correctness~~ of the B specification (e.g. type checking and scope checking) and creates an optimized translation for the validation with TLC.		Moreover it uses static analyses to verify the validity of the B specification (e.g. type checking and scope checking) and creates an optimized translation for the validation with TLC.
	Error traces (e.g. leading to deadlocks or invariant violations) detected by TLC are translated back to B and can be verified by ProB.		Error traces (e.g. leading to deadlocks or invariant violations) detected by TLC are translated back to B and can be verified by ProB.

imported>Jens: /* Overview */

2013-09-23T10:41:33Z

Overview

← Older revision		Revision as of 10:41, 23 September 2013
Line 1:		Line 1:
	== Overview ==		== Overview ==
	~~We think~~ that animation and model checking are important tools when building a model. Animation allows the user to validate if the model corresponds to the user's intentions. Model checking allows to check if the model contains errors and provides counter-examples that help to understand the problem beforehand. Moreover, it allows to reason with domains (like physical units) and verify some properties (like temporal logic ones), that have currently no matching proof support.		Experience with industrial case studies, such as those of WP1 and WP2, have demonstrated that animation and model checking are important tools when building a model. Animation allows the user to validate if the model corresponds to the user's intentions. Model checking allows to check if the model contains errors and provides counter-examples that help to understand the problem beforehand. Moreover, it allows to reason with domains (like physical units) and verify some properties (like temporal logic ones), that have currently no matching proof support.
	The following activities were pursued within the project:		The following activities were pursued within the project:
	* The constraint solving capabilities of ProB have been continuously improved along with scalability improvements.		* The constraint solving capabilities of ProB have been continuously improved along with scalability improvements.

imported>Jens: /* Motivations / Decisions */

2013-09-23T10:38:46Z

Motivations / Decisions

← Older revision		Revision as of 10:38, 23 September 2013
Line 47:		Line 47:

	The work on physical unit support has been completed and is available as an optional plug-in available from the ProB update site.		The work on physical unit support has been completed and is available as an optional plug-in available from the ProB update site.

	~~''' BMotion Studio '''~~

	BMotion Studio provides an easy and fast way to create a visualization for a formal model. It comes with a set of predefined widgets and observer which are sufficient for most visualizations. However, it is still cumbersome to add custom widgets and observer to BMotion Studio, since the user needs programming skills in Java and Eclipse Plugin Development. As a consequence we decided to replace the rendering-engine of BMotion Studio with HTML. This has the benefit that we can use the entire HTML functionality. For instance, HTML elements like tables, buttons and images as well as features like CSS (Cascading Style Sheets) and SVG (Scalable Vector Graphics). In addition, the user can reuse all HTML snippets which can be found in the WWW for his own visualization.
	While the user can create visualizations by writing HTML or SVG, we will also provide a way to create visualizations as in the ''old'' BMotion Studio, i.e. via a visual editor with easy to use dialogues and wizards. The screenshot shows a first prototype of the new BMotion Studio visualizing a model of a simple lift using HTML table elements and SVG elements.

	~~[[File:d33_bms2_prototype.png\|500px\|BMotion Studio 2 Prototype]]~~

	== Available Documentation ==		== Available Documentation ==

imported>Jens: /* Motivations / Decisions */

2013-09-16T08:42:19Z

Motivations / Decisions

← Older revision		Revision as of 08:42, 16 September 2013
Line 51:		Line 51:

	BMotion Studio provides an easy and fast way to create a visualization for a formal model. It comes with a set of predefined widgets and observer which are sufficient for most visualizations. However, it is still cumbersome to add custom widgets and observer to BMotion Studio, since the user needs programming skills in Java and Eclipse Plugin Development. As a consequence we decided to replace the rendering-engine of BMotion Studio with HTML. This has the benefit that we can use the entire HTML functionality. For instance, HTML elements like tables, buttons and images as well as features like CSS (Cascading Style Sheets) and SVG (Scalable Vector Graphics). In addition, the user can reuse all HTML snippets which can be found in the WWW for his own visualization.		BMotion Studio provides an easy and fast way to create a visualization for a formal model. It comes with a set of predefined widgets and observer which are sufficient for most visualizations. However, it is still cumbersome to add custom widgets and observer to BMotion Studio, since the user needs programming skills in Java and Eclipse Plugin Development. As a consequence we decided to replace the rendering-engine of BMotion Studio with HTML. This has the benefit that we can use the entire HTML functionality. For instance, HTML elements like tables, buttons and images as well as features like CSS (Cascading Style Sheets) and SVG (Scalable Vector Graphics). In addition, the user can reuse all HTML snippets which can be found in the WWW for his own visualization.
	While the user can create visualizations by writing HTML or SVG, we will also provide a way to create visualizations as in the ''old'' BMotion Studio, i.e. via a visual editor with easy to use dialogues and wizards. The screenshot shows a first prototype of the new BMotion Studio ~~visualising~~ a model of a simple lift using HTML table elements and SVG elements.		While the user can create visualizations by writing HTML or SVG, we will also provide a way to create visualizations as in the ''old'' BMotion Studio, i.e. via a visual editor with easy to use dialogues and wizards. The screenshot shows a first prototype of the new BMotion Studio visualizing a model of a simple lift using HTML table elements and SVG elements.

	[[File:d33_bms2_prototype.png\|500px\|BMotion Studio 2 Prototype]]		[[File:d33_bms2_prototype.png\|500px\|BMotion Studio 2 Prototype]]

imported>Jens: /* Planning */

2013-09-16T08:40:12Z

Planning

← Older revision		Revision as of 08:40, 16 September 2013
Line 68:		Line 68:


	* We will continue to work on the translation to TLA+ in order to use the TLC model checker. The translation needs to be validated and more of the full classical B language needs to be covered. We will also strive to make TLC available within Rodin for Event-B specifications.		* We will continue to work on the translation of B to TLA+ in order to use the TLC model checker. The translation needs to be validated and more of the full classical B language needs to be covered. We will also strive to make TLC available within Rodin for Event-B specifications.
	* We will also continue to try to add fairness constraints efficiently both to ProB's own model checker and via the translation to TLC.		* We will also continue to try to add fairness constraints efficiently both to ProB's own model checker and via the translation to TLC.
	* ~~Complete~~ BMotionStudio ~~{{TODO}}~~		* We will continue our work on porting BMotionStudio to HTML. We want to define an open architecture that allows re-using BMotionStudio outside of ProB.
	* ~~Improve~~ support for theories with recursive functions; try make recursive functions more efficient.		* We will further improve support for theories with recursive functions and try to make recursive functions more efficient.
	* We will continue evaluating and improving our SAT backend via Kodkod and also evaluate the possibility of using SMT backends.		* We will continue evaluating and improving our SAT backend via Kodkod and also evaluate the possibility of using SMT backends.

imported>Leuschel: /* Planning */

2013-09-16T08:24:56Z

Planning

← Older revision		Revision as of 08:24, 16 September 2013
Line 68:		Line 68:


	- We will continue to work on the translation to TLA+ in order to use the TLC model checker. The translation needs to be validated and more of the full classical B language needs to be covered. We will also strive to make TLC available within Rodin for Event-B specifications.		* We will continue to work on the translation to TLA+ in order to use the TLC model checker. The translation needs to be validated and more of the full classical B language needs to be covered. We will also strive to make TLC available within Rodin for Event-B specifications.
	- We will also continue to try to add fairness constraints efficiently both to ProB's own model checker and via the translation to TLC.		* We will also continue to try to add fairness constraints efficiently both to ProB's own model checker and via the translation to TLC.
	- Complete BMotionStudio {{TODO}}		* Complete BMotionStudio {{TODO}}
	- Improve support for theories with recursive functions; try make recursive functions more efficient.		* Improve support for theories with recursive functions; try make recursive functions more efficient.
			* We will continue evaluating and improving our SAT backend via Kodkod and also evaluate the possibility of using SMT backends.

	== References ==		== References ==

imported>Leuschel: /* Planning */

2013-09-16T08:22:24Z

Planning

← Older revision		Revision as of 08:22, 16 September 2013
Line 66:		Line 66:

	== Planning ==		== Planning ==
	{{TODO}}

			- We will continue to work on the translation to TLA+ in order to use the TLC model checker. The translation needs to be validated and more of the full classical B language needs to be covered. We will also strive to make TLC available within Rodin for Event-B specifications.
			- We will also continue to try to add fairness constraints efficiently both to ProB's own model checker and via the translation to TLC.
			- Complete BMotionStudio {{TODO}}
			- Improve support for theories with recursive functions; try make recursive functions more efficient.

	== References ==		== References ==

imported>Nicolas: Fix title levels

2013-08-27T12:35:52Z

Fix title levels

← Older revision		Revision as of 12:35, 27 August 2013
Line 1:		Line 1:
	= Overview =		== Overview ==
	We think that animation and model checking are important tools when building a model. Animation allows the user to validate if the model corresponds to the user's intentions. Model checking allows to check if the model contains errors and provides counter-examples that help to understand the problem beforehand. Moreover, it allows to reason with domains (like physical units) and verify some properties (like temporal logic ones), that have currently no matching proof support.		We think that animation and model checking are important tools when building a model. Animation allows the user to validate if the model corresponds to the user's intentions. Model checking allows to check if the model contains errors and provides counter-examples that help to understand the problem beforehand. Moreover, it allows to reason with domains (like physical units) and verify some properties (like temporal logic ones), that have currently no matching proof support.
	The following activities were pursued within the project:		The following activities were pursued within the project:
Line 10:		Line 10:
	Outside ADVANCE we improved the model checker by adding support for distributed model checking, partial order reduction and partial guard evaluation. We think that these improvements are also valuable within the ADVANCE project.		Outside ADVANCE we improved the model checker by adding support for distributed model checking, partial order reduction and partial guard evaluation. We think that these improvements are also valuable within the ADVANCE project.

	= Motivations / Decisions =		== Motivations / Decisions ==


Line 55:		Line 55:
	[[File:d33_bms2_prototype.png\|500px\|BMotion Studio 2 Prototype]]		[[File:d33_bms2_prototype.png\|500px\|BMotion Studio 2 Prototype]]

	= Available Documentation =		== Available Documentation ==

	'''ProB'''<br>		'''ProB'''<br>
Line 65:		Line 65:
	A developer-, user documentation, tutorial and examples are available from a dedicated webpage<ref>http://www.stups.uni-duesseldorf.de/bmotionstudio</ref> hosted by the University of Duesseldorf.		A developer-, user documentation, tutorial and examples are available from a dedicated webpage<ref>http://www.stups.uni-duesseldorf.de/bmotionstudio</ref> hosted by the University of Duesseldorf.

	= Planning =		== Planning ==
	{{TODO}}		{{TODO}}

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

	[[Category:ADVANCE D3.3 Deliverable]]		[[Category:ADVANCE D3.3 Deliverable]]

imported>Daniel: /* Motivations / Decisions */

2013-08-25T22:19:04Z

Motivations / Decisions

← Older revision		Revision as of 22:19, 25 August 2013
Line 31:		Line 31:
	often only a part of a model can be translated to Kodkod.		often only a part of a model can be translated to Kodkod.
	We have implemented such a ''slicing'' of the model and plan to validate if this leads to a performance improvement when we use only ProB's constraint solver without Kodkod.		We have implemented such a ''slicing'' of the model and plan to validate if this leads to a performance improvement when we use only ProB's constraint solver without Kodkod.


	'''Theory Plug-in support'''		'''Theory Plug-in support'''

	We adapted ProB to the changes that had been made to the Theory Plug-in in preparation of the upcoming release. We implemented support for the theory of transitive closures.		We adapted ProB to the changes that had been made to the Theory Plug-in in preparation of the upcoming release.
			ProB had support for recursive data types and operators that were defined by direct definitions. Also the SUM and PRODUCT operators were explicitly supported.
			Additionally we implemented now support for the theory of transitive closures.
	From the current set of standard theories, ProB supports animation of models that use operators of the theories "BoolOps", "FixPoint", "Seq", "SUMandPRODUCT" and "closure".		From the current set of standard theories, ProB supports animation of models that use operators of the theories "BoolOps", "FixPoint", "Seq", "SUMandPRODUCT" and "closure".
	Still unsupported are the operators of the remaining standard theories "BinaryTree" and "List" which use recursively defined operators. We plan to implement support for them for the next release.		Still unsupported are the operators of the remaining standard theories "BinaryTree" and "List" which use recursively defined operators. We plan to implement support for them for the next release.

imported>Daniel: /* Motivations / Decisions */ Removed Constraint Solver Improvements: Have to ask Michael about this

2013-08-25T22:15:06Z

Motivations / Decisions: Removed Constraint Solver Improvements: Have to ask Michael about this

← Older revision		Revision as of 22:15, 25 August 2013
Line 32:		Line 32:
	We have implemented such a ''slicing'' of the model and plan to validate if this leads to a performance improvement when we use only ProB's constraint solver without Kodkod.		We have implemented such a ''slicing'' of the model and plan to validate if this leads to a performance improvement when we use only ProB's constraint solver without Kodkod.


	~~{{TODO}}''' Constraint Solver Improvements '''~~
	''During the further development of ProB's constraint solving it became apparent that it would be helpful to represent the cardinality of a set by a CLP(FD) variable. We plan to change ProB's internal representation of sets in a way that its cardinality can be accessed in this way.
	To allow a translation from ProB to Kodkod, we implemented an integer interval analysis. We plan to adapt the analysis to set up sizes of deferred sets. This is necessary because ProB chooses a fixed size for a deferred set and sometimes a model has only solutions for a certain size. Currently a user must supply a size manually.''

	'''Theory Plug-in support'''		'''Theory Plug-in support'''