D23 Introduction - Revision history

imported>Laurent at 11:20, 27 January 2010

2010-01-27T11:20:15Z

← Older revision		Revision as of 11:20, 27 January 2010
Line 6:		Line 6:
	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 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.

	In particular, the WP9 partners ~~strove~~ to meet the following objectives:		In particular, the WP9 partners have strovin to meet the following objectives:
	* 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 16:		Line 16:
	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.		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.

	For each of these newly implemented ~~feature~~ or ~~improvement~~, the document is structured as follows:		For each of these newly implemented features or improvements, the document 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.

imported>Pascal: /* Introduction */

2010-01-27T10:37:53Z

Introduction

← Older revision		Revision as of 10:37, 27 January 2010
Line 4:		Line 4:
	The Rodin platform is available from the 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 is available from the 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 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.

	~~The~~ following items ~~are covered~~: 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.		In particular, the WP9 partners strove to meet the following objectives:
			* 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.
			* 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 checking (ProB), to enable users to find sequences of events that prevent safety properties or proof obligations to be fulfilled.
			* 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.

			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.

	For each of these newly implemented feature or improvement, the document is structured as follows:		For each of these newly implemented feature or improvement, the document is structured as follows:

imported>Pascal: /* Some precisions have been added. */

2010-01-26T16:48:55Z

Some precisions have been added.

← Older revision		Revision as of 16:48, 26 January 2010
Line 4:		Line 4:
	The Rodin platform is available from the 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 is available from the 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~~. Moreover, it summarizes the planned activities~~ for the coming year.		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.

	~~More precisely~~, for each newly implemented feature or improvement, it is structured as follows:		The following items are covered: 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.

			For each of these newly implemented feature or improvement, the document 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.
Line 12:		Line 14:
	* 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 29 Jan 2010) is given.

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

imported>Pascal: /* Sentence making clear that the report includes planned activity. */

2010-01-26T15:14:51Z

Sentence making clear that the report includes planned activity.

← Older revision		Revision as of 15:14, 26 January 2010
Line 4:		Line 4:
	The Rodin platform is available from the 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 is available from the 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.		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. Moreover, it summarizes the planned activities for the coming year.

	~~For~~ each newly implemented feature or improvement, it is structured as follows:		More precisely, for each newly implemented feature or improvement, it 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.

imported>Laurent at 14:47, 6 January 2010

2010-01-06T14:47:05Z

← Older revision		Revision as of 14:47, 6 January 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 is available from the SourceForge site ([~~http://sourceforge.net/project/showfiles.php?group_id=108850&package_id=181714~~ 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 ~~http://wiki.event-b.org~~).		The Rodin platform is available from the 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.		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.

imported>Pascal: /* Punctuation */

2009-12-04T10:00:43Z

Punctuation

← Older revision		Revision as of 10:00, 4 December 2009
Line 9:		Line 9:
	* 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 29 Jan 2010) is given.
	[[Category:D23 Deliverable]]		[[Category:D23 Deliverable]]

imported>Tommy at 14:46, 23 November 2009

2009-11-23T14:46:51Z

← Older revision		Revision as of 14:46, 23 November 2009
Line 9:		Line 9:
	* 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 (eg. 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 29 Jan 2010) is given.
	[[Category:D23 Deliverable]]		[[Category:D23 Deliverable]]

imported>Mathieu: Category:D23 Deliverable

2009-11-16T10:34:13Z

Category:D23 Deliverable

← Older revision		Revision as of 10:34, 16 November 2009
Line 12:		Line 12:
	* 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 29 Jan 2010) is given.
			[[Category:D23 Deliverable]]

imported>Pascal: /* Creation */

2009-11-16T09:58:23Z

Creation

New page

The deliverable D23 of the DEPLOY project is split into two parts:
* The Rodin core platform and plug-ins (i.e. the DEPLOY tools).
* This document.
The Rodin platform is available from the SourceForge site ([http://sourceforge.net/project/showfiles.php?group_id=108850&package_id=181714 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 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.

For each newly implemented feature or improvement, it is structured as follows:
* 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.
* Choices / decisions. The decisions (eg. design decisions) are justified
* 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.