D32 Introduction - Revision history

imported>Laurent at 17:03, 24 November 2010

2010-11-24T17:03:20Z

imported>Tommy at 15:52, 23 November 2010

2010-11-23T15:52:57Z

← Older revision		Revision as of 15:52, 23 November 2010
Line 8:		Line 8:
	Among the aims that WP9 partners reached, it might be worth to cite :		Among the aims that WP9 partners reached, it might be worth to cite :
	* Improved scalability and teamwork ability of the Rodin platform to support industrial deployments, through GUI refactorings and new features, SVN model storage, decomposition, modularisation, flows support, as well as qualitative probabilistic reasoning and others,		* Improved scalability and teamwork ability of the Rodin platform to support industrial deployments, through GUI refactorings and new features, SVN model storage, decomposition, modularisation, flows support, as well as qualitative probabilistic reasoning and others,
	* Mathematical extensions ~~can~~ now ~~be used~~ in Rodin. The core of the Rodin platform has been modified and the Theory plug-in has been developed to allow the definition of basic predicates, new operators or new algebraic types.		* Mathematical extensions are now supported in Rodin. The core of the Rodin platform has been modified and the Theory plug-in has been developed to allow the definition of basic predicates, new operators or new algebraic types,
	* Prover performance increased through the addition of a relevance filtering plug-in which raised the number of automatically discharged proof obligations. Moreover, work has been done to establish the soundness of provers and improve the well-definition proof obligation generation,		* Prover performance increased through the addition of a relevance filtering plug-in which raised the number of automatically discharged proof obligations. Moreover, work has been done to establish the soundness of provers and improve the well-definition proof obligation generation,
	* Model animation has been improved, now supports multi-level animation and has been applied in WP1-4 partner's case studies,		* Model animation has been improved, now supports multi-level animation and has been applied in WP1-4 partner's case studies,

imported>Tommy at 15:51, 23 November 2010

2010-11-23T15:51:50Z

← Older revision		Revision as of 15:51, 23 November 2010
Line 4:		Line 4:
	The Rodin platform can be downloaded from SourceForge site ([http://sourceforge.net/project/showfiles.php?group_id=108850&package_id=181714]). The Event-B wiki ([http://wiki.event-b.org]) hosts the documentation of the tool.		The Rodin platform can be downloaded from SourceForge site ([http://sourceforge.net/project/showfiles.php?group_id=108850&package_id=181714]). The Event-B wiki ([http://wiki.event-b.org]) hosts the documentation of the tool.

	This document gives an insight into the work achieved throughout the WP9 ''Tooling research and development'' work package, during the third year of the DEPLOY project (Feb 2010-Jan 2011), and depicts the WP9 partner's objectives for the coming and last year of ~~DEPLOY~~.		This document gives an insight into the work achieved throughout the WP9 ''Tooling research and development'' work package, during the third year of the DEPLOY project (Feb 2010-Jan 2011), and depicts the WP9 partner's objectives for the coming and last year of the project.

	Among the aims that WP9 partners reached, it might be worth to cite :		Among the aims that WP9 partners reached, it might be worth to cite :

imported>Tommy at 14:53, 19 November 2010

2010-11-19T14:53:28Z

← Older revision		Revision as of 14:53, 19 November 2010
Line 8:		Line 8:
	Among the aims that WP9 partners reached, it might be worth to cite :		Among the aims that WP9 partners reached, it might be worth to cite :
	* Improved scalability and teamwork ability of the Rodin platform to support industrial deployments, through GUI refactorings and new features, SVN model storage, decomposition, modularisation, flows support, as well as qualitative probabilistic reasoning and others,		* Improved scalability and teamwork ability of the Rodin platform to support industrial deployments, through GUI refactorings and new features, SVN model storage, decomposition, modularisation, flows support, as well as qualitative probabilistic reasoning and others,
	* Mathematical extensions,		* Mathematical extensions can now be used in Rodin. The core of the Rodin platform has been modified and the Theory plug-in has been developed to allow the definition of basic predicates, new operators or new algebraic types.
	* Prover performance~~, to increase~~ the number of automatically discharged proof obligations. ~~A relevance filtering tool has been developed~~, ~~and~~ work has been done to establish the soundness of provers and improve the well-definition proof obligation generation,		* Prover performance increased through the addition of a relevance filtering plug-in which raised the number of automatically discharged proof obligations. Moreover, work has been done to establish the soundness of provers and improve the well-definition proof obligation generation,
	* Model animation and testing, ~~to validate Event-B models.{{TODO}} Refactor~~		* Model animation has been improved, now supports multi-level animation and has been applied in WP1-4 partner's case studies,
	* Records,		* Model testing was guided by the needs of WP1-4 partners and several approaches have been investigated,
			* Structured types can now be directly defined and used in Rodin through the Records plug-in,
	* UML is thighter integrated in Rodin, through new features implementation or even the state-machine animation,		* UML is thighter integrated in Rodin, through new features implementation or even the state-machine animation,
	* Code generation, to enable complete support for development, from high-level Event-B models down to executable implementations. An demonstrator tool has been developed.		* Code generation, to enable complete support for development, from high-level Event-B models down to executable implementations. An demonstrator tool has been developed.

imported>Tommy at 14:32, 19 November 2010

2010-11-19T14:32:51Z

← Older revision		Revision as of 14:32, 19 November 2010
Line 2:		Line 2:
	* the Rodin core platform and plug-ins (i.e. the DEPLOY tools),		* the Rodin core platform and plug-ins (i.e. the DEPLOY tools),
	* this document.		* this document.
	The Rodin platform can be downloaded from SourceForge site ([http://sourceforge.net/project/showfiles.php?group_id=108850&package_id=181714]). The ~~tool documentation is provided within the~~ Event-B wiki ([http://wiki.event-b.org]).		The Rodin platform can be downloaded from SourceForge site ([http://sourceforge.net/project/showfiles.php?group_id=108850&package_id=181714]). The Event-B wiki ([http://wiki.event-b.org]) hosts the documentation of the tool.

	This document gives an insight into the work achieved throughout the WP9 ''Tooling research and development'' work package, during the third year of the DEPLOY project (Feb 2010-Jan 2011), and depicts the WP9 partner's objectives for the coming and last year of DEPLOY.		This document gives an insight into the work achieved throughout the WP9 ''Tooling research and development'' work package, during the third year of the DEPLOY project (Feb 2010-Jan 2011), and depicts the WP9 partner's objectives for the coming and last year of DEPLOY.

imported>Tommy at 14:30, 19 November 2010

2010-11-19T14:30:38Z

← Older revision		Revision as of 14:30, 19 November 2010
Line 7:		Line 7:

	Among the aims that WP9 partners reached, it might be worth to cite :		Among the aims that WP9 partners reached, it might be worth to cite :
	~~{{TODO}} Refactor this part.~~		* Improved scalability and teamwork ability of the Rodin platform to support industrial deployments, through GUI refactorings and new features, SVN model storage, decomposition, modularisation, flows support, as well as qualitative probabilistic reasoning and others,
	* Improved scalability of the Rodin platform to support industrial deployments, through GUI ~~enhancements (smart completion~~, ~~renaming~~, ~~text editing~~, ~~etc)~~, ~~decomposition~~ support and ~~design-pattern management.~~		* Mathematical extensions,
	* Prover ~~integrity and~~ performance, to ~~enhance~~ the ~~confidence in provers~~ and to ~~enlarge their proving capabilities. To this aim,~~ the ~~existing~~ provers ~~have been improved~~ and ~~a new rule~~-~~based prover plug-in has been implemented.~~		* Prover performance, to increase the number of automatically discharged proof obligations. A relevance filtering tool has been developed, and work has been done to establish the soundness of provers and improve the well-definition proof obligation generation,
	* Model animation and testing, to validate Event-B models. More precisely, the ProB or AnimB plug-ins allow a domain expert to detect errors in a model and ensure the presence of desired functionalities. Moreover, it is very important for many industrial applications to be able to completely hide the underlying formal specification.		* Model animation and testing, to validate Event-B models.{{TODO}} Refactor
	* ~~Model checking (ProB)~~, ~~to enable users to find sequences of events that prevent safety properties or proof obligations to be fulfilled.~~		* Records,
	* UML ~~integration. UML~~-~~B provides a diagrammatic~~, ~~formal modelling notation based on UML.~~		* UML is thighter integrated in Rodin, through new features implementation or even the state-machine animation,
	* Code generation, to enable complete support for development, from high-level Event-B models down to executable implementations. An ~~initial definition of language support for code generation~~ has been ~~put forward~~.		* Code generation, to enable complete support for development, from high-level Event-B models down to executable implementations. An demonstrator tool has been developed.
	~~----~~

	The various parts making up this document are the following: general platform maintenance, mathematical extensions, provers, UML-B improvements, code generation, teamwork, scalability, model animation, and model-based testing.		The various parts making up this document are the following: general platform maintenance, mathematical extensions, provers, UML-B improvements, code generation, teamwork, scalability, model animation, and model-based testing.

imported>Tommy at 14:04, 19 November 2010

2010-11-19T14:04:20Z

← Older revision		Revision as of 14:04, 19 November 2010
Line 4:		Line 4:
	The Rodin platform can be downloaded from SourceForge site ([http://sourceforge.net/project/showfiles.php?group_id=108850&package_id=181714]). The tool documentation is provided within the Event-B wiki ([http://wiki.event-b.org]).		The Rodin platform can be downloaded from SourceForge site ([http://sourceforge.net/project/showfiles.php?group_id=108850&package_id=181714]). The tool documentation is provided within the Event-B wiki ([http://wiki.event-b.org]).

	This document gives an insight into the work achieved throughout the WP9 ''Tooling research and development'' work package, during the third year of the DEPLOY project (Feb 2010-Jan 2011), and depicts the WP9 partner's objectives for the coming year.		This document gives an insight into the work achieved throughout the WP9 ''Tooling research and development'' work package, during the third year of the DEPLOY project (Feb 2010-Jan 2011), and depicts the WP9 partner's objectives for the coming and last year of DEPLOY.

	Among the aims that WP9 partners reached, it might be worth to cite :		Among the aims that WP9 partners reached, it might be worth to cite :

imported>Tommy at 13:46, 19 November 2010

2010-11-19T13:46:22Z

← Older revision		Revision as of 13:46, 19 November 2010
Line 25:		Line 25:
	* Planning. A timeline and the current status (as of 28 Jan 2011) is given.		* Planning. A timeline and the current status (as of 28 Jan 2011) is given.

	[[Category:~~D23~~ Deliverable]]		[[Category:D32 Deliverable]]

imported>Tommy at 13:09, 19 November 2010

2010-11-19T13:09:31Z

← Older revision		Revision as of 13:09, 19 November 2010
Line 1:		Line 1:
	The DEPLOY's D32 deliverable is composed of:		The DEPLOY's D32 deliverable is composed of:
	* ~~The~~ Rodin core platform and plug-ins (i.e. the DEPLOY tools).		* the Rodin core platform and plug-ins (i.e. the DEPLOY tools),
	* ~~This~~ document.		* this document.
	The Rodin platform can be downloaded from SourceForge site ([http://sourceforge.net/project/showfiles.php?group_id=108850&package_id=181714]). The tool documentation is provided within the Event-B wiki ([http://wiki.event-b.org]).		The Rodin platform can be downloaded from SourceForge site ([http://sourceforge.net/project/showfiles.php?group_id=108850&package_id=181714]). The tool documentation is provided within the Event-B wiki ([http://wiki.event-b.org]).

imported>Tommy at 13:04, 19 November 2010

2010-11-19T13:04:25Z

← Older revision		Revision as of 13:04, 19 November 2010
Line 4:		Line 4:
	The Rodin platform can be downloaded from SourceForge site ([http://sourceforge.net/project/showfiles.php?group_id=108850&package_id=181714]). The tool documentation is provided within the Event-B wiki ([http://wiki.event-b.org]).		The Rodin platform can be downloaded from SourceForge site ([http://sourceforge.net/project/showfiles.php?group_id=108850&package_id=181714]). The tool documentation is provided within the Event-B wiki ([http://wiki.event-b.org]).

	This document gives ~~a description of~~ the work ~~that was carried on~~ during the ~~second~~ year of the DEPLOY project (Feb ~~2009~~-Jan ~~2010~~), ~~in the course of~~ the WP9 '~~'Tooling research and development'' work package, and brings new perspectives~~ for the coming year.		This document gives an insight into the work achieved throughout the WP9 ''Tooling research and development'' work package, during the third year of the DEPLOY project (Feb 2010-Jan 2011), and depicts the WP9 partner's objectives for the coming year.

	~~In particular,~~ the WP9 partners ~~have strovin~~ to ~~meet the following objectives~~:		Among the aims that WP9 partners reached, it might be worth to cite :
			{{TODO}} Refactor this part.
	* Improved scalability of the Rodin platform to support industrial deployments, through GUI enhancements (smart completion, renaming, text editing, etc), decomposition support and design-pattern management.		* Improved scalability of the Rodin platform to support industrial deployments, through GUI enhancements (smart completion, renaming, text editing, etc), decomposition support and design-pattern management.
	* Prover integrity and performance, to enhance the confidence in provers and to enlarge their proving capabilities. To this aim, the existing provers have been improved and a new rule-based prover plug-in has been implemented.		* Prover integrity and performance, to enhance the confidence in provers and to enlarge their proving capabilities. To this aim, the existing provers have been improved and a new rule-based prover plug-in has been implemented.
Line 13:		Line 14:
	* UML integration. UML-B provides a diagrammatic, formal modelling notation based on UML.		* UML integration. UML-B provides a diagrammatic, formal modelling notation based on UML.
	* Code generation, to enable complete support for development, from high-level Event-B models down to executable implementations. An initial definition of language support for code generation has been put forward.		* Code generation, to enable complete support for development, from high-level Event-B models down to executable implementations. An initial definition of language support for code generation has been put forward.
			----

	~~This~~ document ~~covers~~ the following ~~items~~: general platform maintenance, UML-B improvements, ~~ProB improvements, text editor plug-in, decomposition plug-in, initial definition of language support for~~ code generation, ~~improvements to existing provers~~, ~~rule-based prover~~, ~~pattern plug-in~~, ~~flow plug-in~~ and ~~modularisation plug~~-in.		The various parts making up this document are the following: general platform maintenance, mathematical extensions, provers, UML-B improvements, code generation, teamwork, scalability, model animation, and model-based testing.

	~~For~~ each of these ~~newly implemented features or~~ improvements, ~~the document~~ is structured as follows:		Note that each of these parts is describing the improvements made, and is structured as follows:
	* Overview. The involved partners are identified and an overview of the contribution is given.		* Overview. The involved partners are identified and an overview of the contribution is given.
	* Motivations. The motivations for each tool extension and improvement are expressed.		* Motivations. The motivations for each tool extension and improvement are expressed.
	* Choices / decisions. The decisions (e.g. design decisions) are justified.		* Choices / decisions. The decisions (e.g. design decisions) are justified.
	* Available documentation. Some pointers to the Event-B wiki or related publications are listed.		* Available documentation. Some pointers to the Event-B wiki or related publications are listed.
	* Planning. A timeline and the current status (as of 29 Jan ~~2010~~) is given.		* Planning. A timeline and the current status (as of 28 Jan 2011) is given.

	[[Category:D23 Deliverable]]		[[Category:D23 Deliverable]]

← Older revision		Revision as of 17:03, 24 November 2010
Line 1:		Line 1:
	The DEPLOY's D32 ~~deliverable~~ is composed of:		The DEPLOY deliverable D32 is composed of:
	* the Rodin core platform and plug-ins (i.e. the DEPLOY tools),		* the Rodin core platform and plug-ins (i.e. the DEPLOY tools),
	* this document.		* this document.
	The Rodin platform can be downloaded from SourceForge site ([http://sourceforge.net/project/showfiles.php?group_id=108850&package_id=181714]). The Event-B wiki ([http://wiki.event-b.org]) hosts the documentation of the tool.		The Rodin platform can be downloaded from the SourceForge site ([http://sourceforge.net/project/showfiles.php?group_id=108850&package_id=181714]). The Event-B wiki ([http://wiki.event-b.org]) hosts the documentation of the tool.

	This document gives an insight into the work achieved throughout the WP9 ''Tooling research and development'' work package, during the third year of the DEPLOY project (Feb 2010-Jan 2011), and depicts the WP9 partner's objectives for the coming and last year of the project.		This document gives an insight into the work achieved throughout the WP9 ''Tooling research and development'' work package, during the third year of the DEPLOY project (Feb 2010-Jan 2011), and depicts the WP9 partner's objectives for the coming and last year of the project.

	Among the aims that WP9 partners reached, it ~~might be~~ worth ~~to cite~~ :		Among the aims that WP9 partners reached in the past year, it is worth citing :
	* Improved scalability and teamwork ability of the Rodin platform to support industrial deployments, through GUI ~~refactorings~~ and new features, ~~SVN~~ model storage, decomposition, modularisation, ~~flows~~ support, as well as qualitative probabilistic reasoning and others,		* Improved scalability and teamwork ability of the Rodin platform to support industrial deployments, through GUI refactoring and new features, Subversion model storage, decomposition, modularisation, flow support, as well as qualitative probabilistic reasoning and others,
	* Mathematical extensions are now supported in Rodin. The core of the Rodin platform has been modified and the Theory plug-in has been developed to allow the definition of basic predicates, new operators or new algebraic types,		* Mathematical extensions are now supported in Rodin. The core of the Rodin platform has been modified and the Theory plug-in has been developed to allow the definition of new basic predicates, new operators and new algebraic types,
	* Prover performance increased through the addition of a relevance filtering plug-in which ~~raised~~ the number of automatically discharged proof obligations. Moreover, work has been done to establish the soundness of provers and improve the well-~~definition~~ proof ~~obligation generation~~,		* Prover performance has increased through the addition of a relevance filtering plug-in which raises the number of automatically discharged proof obligations. Moreover, work has been done to establish the soundness of provers and improve the generation of well-definedness proof obligations,
	* Model animation has been improved, now supports multi-level animation and has been applied in WP1-4 ~~partner's case studies~~,		* Model animation has been improved: it now supports multi-level animation and has been applied in WP1-4 deployment workpackages,
	* Model testing was guided by the needs of WP1-4 partners and several approaches have been investigated,		* Model testing was guided by the needs of WP1-4 partners and several approaches have been investigated,
	* Structured types can now be directly defined and used in Rodin through the Records plug-in,		* Structured types can now be directly defined and used in Rodin through the Records plug-in,
	* UML is ~~thighter~~ integrated in Rodin, through new features implementation or ~~even the~~ state-machine animation,		* UML is more tightly integrated in Rodin, through new features implementation or state-machine animation,
	* Code generation, to enable complete support for development, from high-level Event-B models down to executable implementations. An demonstrator tool has been developed.		* Code generation, to enable complete support for development, from high-level Event-B models down to executable implementations. A demonstrator tool has been developed.

	The various parts making up this document are the following: general platform maintenance, mathematical extensions, provers, UML-B improvements, code generation, teamwork, scalability, model animation, and model-based testing.		The various parts making up this document are the following: general platform maintenance, mathematical extensions, provers, UML-B improvements, code generation, teamwork, scalability, model animation, and model-based testing.