ADVANCE D3.2 Introduction - Revision history

imported>Tommy at 16:27, 13 July 2012

2012-07-13T16:27:27Z

← Older revision		Revision as of 16:27, 13 July 2012
Line 1:		Line 1:
	The ADVANCE D3.2 deliverable is composed of the present document and the Rodin toolset. The considered Rodin toolset ~~consits~~ of the Rodin core platform and the plug-ins created or maintained in the frame of the ADVANCE project. Other plug-ins, available for the Rodin platform but not maintained within the ADVANCE project, are not taken into account within this deliverable.		The ADVANCE D3.2 deliverable is composed of the present document and the Rodin toolset. The considered Rodin toolset consists of the Rodin core platform and the plug-ins created or maintained in the frame of the ADVANCE project. Other plug-ins, available for the Rodin platform but not maintained within the ADVANCE project, are not taken into account within this deliverable.

	The Rodin platform can be downloaded from the SourceForge site.<ref>http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform</ref><br>		The Rodin platform can be downloaded from the SourceForge site.<ref>http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform</ref><br>

imported>Laurent at 15:00, 28 June 2012

2012-06-28T15:00:58Z

← Older revision		Revision as of 15:00, 28 June 2012
Line 1:		Line 1:
	The ADVANCE D3.2 deliverable is composed of the present document and the Rodin toolset. The considered Rodin toolset consits of the Rodin core platform and the plug-ins created or maintained in the frame of the ADVANCE project. ~~Indeed, there are contributed~~ plug-ins available for the Rodin ~~core~~ platform ~~which are~~ not maintained within the ADVANCE project, ~~therefore should~~ not be taken into account within this deliverable.		The ADVANCE D3.2 deliverable is composed of the present document and the Rodin toolset. The considered Rodin toolset consits of the Rodin core platform and the plug-ins created or maintained in the frame of the ADVANCE project. Other plug-ins, available for the Rodin platform but not maintained within the ADVANCE project, are not taken into account within this deliverable.

	The Rodin platform can be downloaded from the SourceForge site.<ref>http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform</ref><br>		The Rodin platform can be downloaded from the SourceForge site.<ref>http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform</ref><br>
Line 8:		Line 8:

	The present document intends to give a relevant overview of the work achieved within the work package 3: ''Methods and Tools for Model Construction and Proof'', during the first ten months of the ADVANCE project (Oct 2011 - Jul 2011), and aims to let the reader get a glimpse of the WP3 member's contribution plans and objectives.		The present document intends to give a relevant overview of the work achieved within the work package 3: ''Methods and Tools for Model Construction and Proof'', during the first ten months of the ADVANCE project (Oct 2011 - Jul 2011), and aims to let the reader get a glimpse of the WP3 member's contribution plans and objectives.
	It is worth reminding that the ADVANCE project time frame overlapped the end of the EU FP7 DEPLOY project<ref>http://www.deploy-project.eu</ref> from October 2011 to April 2012. Therefore, the commitment of WP3 members that were members of DEPLOY tooling workpackage as well, was mainly devoted during this period to consolidate the toolset by fixing the identified bugs and ~~rectigying~~ usability issues. These activities encompass the objectives of the task 3.2 mentionned in the ADVANCE Description of Work (DoW).		It is worth reminding that the ADVANCE project time frame overlapped the end of the EU FP7 DEPLOY project<ref>http://www.deploy-project.eu</ref> from October 2011 to April 2012. Therefore, the commitment of WP3 members that were members of the DEPLOY tooling workpackage as well, was mainly devoted during this period to consolidate the toolset by fixing the identified bugs and mitigating usability issues. These activities encompass the objectives of the task 3.2 mentionned in the ADVANCE Description of Work (DoW).

	The document is divided into four parts: general platform maintenance, improvement of automated proof, language extension, model checking, and model composition and decomposition.		The document is divided into four parts: general platform maintenance, improvement of automated proof, language extension, model checking, and model composition and decomposition.

	The common structure ~~that~~ is ~~reuse~~ for each contribution ~~in the general platform maintenance part and later, in~~ the ~~other part could be detailed as follows~~:		The common structure which is used for each contribution is the following:
	* 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 / Decisions. The motivation for each tool extension and improvement are expressed. The decisions (e.g. design decision) are related.		* Motivations / Decisions. The motivation for each tool extension and improvement are expressed. The decisions (e.g. design decision) are related.

imported>Tommy at 15:37, 25 June 2012

2012-06-25T15:37:15Z

← Older revision		Revision as of 15:37, 25 June 2012
Line 2:		Line 2:

	The Rodin platform can be downloaded from the SourceForge site.<ref>http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform</ref><br>		The Rodin platform can be downloaded from the SourceForge site.<ref>http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform</ref><br>
	Moreover, the platform includes a collaborative documentation that is collected from two maintained locations :		Moreover, the platform includes a collaborative documentation that is collected from two maintained locations:
	* the Event-B wiki,<ref name="EventB_wiki">http://wiki.event-b.org</ref>		* the Event-B wiki,<ref name="EventB_wiki">http://wiki.event-b.org</ref>
	* the Rodin Handbook.<ref name="Rodin_handbook_Page">http://handbook.event-b.org</ref>		* the Rodin Handbook.<ref name="Rodin_handbook_Page">http://handbook.event-b.org</ref>

imported>Tommy at 15:07, 25 June 2012

2012-06-25T15:07:28Z

← Older revision		Revision as of 15:07, 25 June 2012
Line 1:		Line 1:
	The ADVANCE D3.2 deliverable is composed of the present document and the Rodin toolset. The considered Rodin toolset consits of the Rodin core platform and the plug-ins created or maintained in the frame of the ADVANCE project. Indeed, there are contributed plug-ins available for the Rodin core platform which are not maintained within the ADVANCE project, therefore should not be taken into account within this deliverable.		The ADVANCE D3.2 deliverable is composed of the present document and the Rodin toolset. The considered Rodin toolset consits of the Rodin core platform and the plug-ins created or maintained in the frame of the ADVANCE project. Indeed, there are contributed plug-ins available for the Rodin core platform which are not maintained within the ADVANCE project, therefore should not be taken into account within this deliverable.

	The Rodin platform can be downloaded from the SourceForge site<ref>http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform</ref>.<br>		The Rodin platform can be downloaded from the SourceForge site.<ref>http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform</ref><br>
	Moreover, the platform includes a collaborative documentation that is collected from two maintained locations :		Moreover, the platform includes a collaborative documentation that is collected from two maintained locations :
	* the Event-B wiki<ref name="EventB_wiki">http://wiki.event-b.org</ref>,		* the Event-B wiki,<ref name="EventB_wiki">http://wiki.event-b.org</ref>
	* the Rodin Handbook<ref name="Rodin_handbook_Page">http://handbook.event-b.org</ref>.		* the Rodin Handbook.<ref name="Rodin_handbook_Page">http://handbook.event-b.org</ref>
	These locations can be consulted from outside the Rodin tool.		These locations can be consulted from outside the Rodin tool.

imported>Tommy at 12:55, 21 June 2012

2012-06-21T12:55:52Z

← Older revision		Revision as of 12:55, 21 June 2012
Line 12:		Line 12:
	The document is divided into four parts: general platform maintenance, improvement of automated proof, language extension, model checking, and model composition and decomposition.		The document is divided into four parts: general platform maintenance, improvement of automated proof, language extension, model checking, and model composition and decomposition.

	~~Note~~ that each ~~of these parts is describing~~ the ~~improvements made~~, ~~and is structured~~ as follows:		The common structure that is reuse for each contribution in the general platform maintenance part and later, in the other part could be detailed 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 / Decisions. The motivation for each tool extension and improvement are expressed. The decisions (e.g. design decision) are related.		* Motivations / Decisions. The motivation for each tool extension and improvement are expressed. The decisions (e.g. design decision) are related.

imported>Tommy at 12:54, 21 June 2012

2012-06-21T12:54:00Z

← Older revision		Revision as of 12:54, 21 June 2012
Line 10:		Line 10:
	It is worth reminding that the ADVANCE project time frame overlapped the end of the EU FP7 DEPLOY project<ref>http://www.deploy-project.eu</ref> from October 2011 to April 2012. Therefore, the commitment of WP3 members that were members of DEPLOY tooling workpackage as well, was mainly devoted during this period to consolidate the toolset by fixing the identified bugs and rectigying usability issues. These activities encompass the objectives of the task 3.2 mentionned in the ADVANCE Description of Work (DoW).		It is worth reminding that the ADVANCE project time frame overlapped the end of the EU FP7 DEPLOY project<ref>http://www.deploy-project.eu</ref> from October 2011 to April 2012. Therefore, the commitment of WP3 members that were members of DEPLOY tooling workpackage as well, was mainly devoted during this period to consolidate the toolset by fixing the identified bugs and rectigying usability issues. These activities encompass the objectives of the task 3.2 mentionned in the ADVANCE Description of Work (DoW).

	~~Although, it is worth citing :~~		The document is divided into four parts: general platform maintenance, improvement of automated proof, language extension, model checking, and model composition and decomposition.
	~~• Increasing usability and of the toolset was the main targets regarding scalability.~~
	~~They have been obtained through major core and UI refactorings.~~
	~~• A Model-Based Testing plug-in whose development was guided by the needs of WP1-4~~
	~~partners has been released and documented.~~
	~~• Increasing prover performance through the addition of several rewriting or inference rules, as~~
	~~well as two plug-ins, the Export to Isabelle and SMT Solvers which both help to raise the~~
	~~number of automatically discharged proof obligations.~~
	~~• An enhanced proving experience, and proving ability with the introduction of user~~
	~~customizable and parametrizable tactic profiles.~~

	* 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 new basic predicates, new operators and new algebraic types,~~
	* 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: 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,
	* Structured types can now be directly defined and used in Rodin through the Records plug-in,
	* 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. 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~~.

	Note that each of these parts is describing the improvements made, and 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 / Decisions. The motivation for each tool extension and improvement are expressed. The decisions (e.g. design decision) are related.
	* Choices / decisions. The decisions (e.g. design ~~decisions~~) are ~~justified~~.		* Available documentation. Some pointers to the available documentation or related publications are listed.
	* Available documentation. Some pointers to the ~~Event-B wiki~~ or related publications are listed.		* Planning. The current status about the topic (as of July 2012), and an overview of the future plans are given.
	* Planning. ~~A timeline and the~~ current status (as of ~~28 Jan 2011~~) is given.


	== References ==		== References ==

imported>Tommy at 12:42, 21 June 2012

2012-06-21T12:42:36Z

← Older revision		Revision as of 12:42, 21 June 2012
Line 1:		Line 1:
	The ADVANCE D3.2 deliverable is composed of the present document and the Rodin toolset. The considered Rodin toolset consits of the Rodin core platform and the plug-ins created or maintained in the frame of the ADVANCE project. Indeed, there are contributed plug-ins available for the Rodin core platform which are not maintained within the ADVANCE project, therefore should not be taken into account within this deliverable.		The ADVANCE D3.2 deliverable is composed of the present document and the Rodin toolset. The considered Rodin toolset consits of the Rodin core platform and the plug-ins created or maintained in the frame of the ADVANCE project. Indeed, there are contributed plug-ins available for the Rodin core platform which are not maintained within the ADVANCE project, therefore should not be taken into account within this deliverable.

	The Rodin platform can be downloaded from the SourceForge site<ref>http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform</ref>. Moreover, the platform includes a collaborative documentation that is collected from two maintained locations :		The Rodin platform can be downloaded from the SourceForge site<ref>http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform</ref>.<br>
			Moreover, the platform includes a collaborative documentation that is collected from two maintained locations :
	* the Event-B wiki<ref name="EventB_wiki">http://wiki.event-b.org</ref>,		* the Event-B wiki<ref name="EventB_wiki">http://wiki.event-b.org</ref>,
	* the Rodin Handbook<ref name="Rodin_handbook_Page">http://handbook.event-b.org</ref>.		* the Rodin Handbook<ref name="Rodin_handbook_Page">http://handbook.event-b.org</ref>.
	These locations can be consulted from outside the Rodin tool.		These locations can be consulted from outside the Rodin tool.

	The present document intends to give a ~~significant~~ overview of the work achieved within the ~~WP3~~ ''~~Tooling research~~ and ~~development~~'' ~~work package~~, during the first ten months of the ADVANCE project (Oct 2011 - Jul 2011), and aims to let the reader get a glimpse of the WP3 member's contribution plans and objectives.		The present document intends to give a relevant overview of the work achieved within the work package 3: ''Methods and Tools for Model Construction and Proof'', during the first ten months of the ADVANCE project (Oct 2011 - Jul 2011), and aims to let the reader get a glimpse of the WP3 member's contribution plans and objectives.
			It is worth reminding that the ADVANCE project time frame overlapped the end of the EU FP7 DEPLOY project<ref>http://www.deploy-project.eu</ref> from October 2011 to April 2012. Therefore, the commitment of WP3 members that were members of DEPLOY tooling workpackage as well, was mainly devoted during this period to consolidate the toolset by fixing the identified bugs and rectigying usability issues. These activities encompass the objectives of the task 3.2 mentionned in the ADVANCE Description of Work (DoW).

	It is worth reminding that the ADVANCE project time frame overlaped with the end of the EU FP7 DEPLOY project<ref>http://www.deploy-project.eu</ref>. Therefore, the WP3 members that where also members of DEPLOY committed to ...		Although, it is worth citing :

	~~Among the aims that DE partners reached in the past year~~, it is worth citing :
	• Increasing usability and of the toolset was the main targets regarding scalability.		• Increasing usability and of the toolset was the main targets regarding scalability.
	They have been obtained through major core and UI refactorings.		They have been obtained through major core and UI refactorings.

imported>Tommy at 10:33, 21 June 2012

2012-06-21T10:33:09Z

← Older revision		Revision as of 10:33, 21 June 2012
Line 1:		Line 1:
	The ADVANCE D3.2 deliverable is composed of the present document and the Rodin toolset. The considered Rodin toolset consits of the Rodin core platform and the plug-ins created or maintained in the frame of the ADVANCE project. Indeed, there are contributed plug-ins available for the Rodin core platform which are not maintained within the ADVANCE project, therefore should not be taken into account within this deliverable.		The ADVANCE D3.2 deliverable is composed of the present document and the Rodin toolset. The considered Rodin toolset consits of the Rodin core platform and the plug-ins created or maintained in the frame of the ADVANCE project. Indeed, there are contributed plug-ins available for the Rodin core platform which are not maintained within the ADVANCE project, therefore should not be taken into account within this deliverable.

	The Rodin platform can be downloaded from the SourceForge site<ref>http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/</ref>. Moreover, the platform includes a collaborative documentation that is collected from two maintained locations :		The Rodin platform can be downloaded from the SourceForge site<ref>http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform</ref>. Moreover, the platform includes a collaborative documentation that is collected from two maintained locations :
	* the Event-B wiki<ref name="EventB_wiki">http://wiki.event-b.org</ref>,		* the Event-B wiki<ref name="EventB_wiki">http://wiki.event-b.org</ref>,
	* the Rodin Handbook<ref name="Rodin_handbook_Page">http://handbook.event-b.org</ref>.		* the Rodin Handbook<ref name="Rodin_handbook_Page">http://handbook.event-b.org</ref>.
Line 8:		Line 8:
	The present document intends to give a significant overview of the work achieved within the WP3 ''Tooling research and development'' work package, during the first ten months of the ADVANCE project (Oct 2011 - Jul 2011), and aims to let the reader get a glimpse of the WP3 member's contribution plans and objectives.		The present document intends to give a significant overview of the work achieved within the WP3 ''Tooling research and development'' work package, during the first ten months of the ADVANCE project (Oct 2011 - Jul 2011), and aims to let the reader get a glimpse of the WP3 member's contribution plans and objectives.

	It is worth ~~to remind~~ that the ADVANCE project time frame overlaped with... ~~blablabla {{TODO~~: ~~Continue after lunch}}~~		It is worth reminding that the ADVANCE project time frame overlaped with the end of the EU FP7 DEPLOY project<ref>http://www.deploy-project.eu</ref>. Therefore, the WP3 members that where also members of DEPLOY committed to ...

			Among the aims that DE partners reached in the past year, it is worth citing :
			• Increasing usability and of the toolset was the main targets regarding scalability.
			They have been obtained through major core and UI refactorings.
			• A Model-Based Testing plug-in whose development was guided by the needs of WP1-4
			partners has been released and documented.
			• Increasing prover performance through the addition of several rewriting or inference rules, as
			well as two plug-ins, the Export to Isabelle and SMT Solvers which both help to raise the
			number of automatically discharged proof obligations.
			• An enhanced proving experience, and proving ability with the introduction of user
			customizable and parametrizable tactic profiles.

	~~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 refactoring and new features, Subversion model storage, decomposition, modularisation, flow 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 new basic predicates, new operators and 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,

imported>Tommy at 10:24, 21 June 2012

2012-06-21T10:24:56Z

← Older revision		Revision as of 10:24, 21 June 2012
Line 1:		Line 1:
	The ADVANCE D3.2 deliverable is composed of the present document and the Rodin toolset. The considered Rodin toolset consits of the Rodin core platform and the plug-ins created or maintained in the frame of the ADVANCE project. Indeed, there are contributed plug-ins available for the Rodin core platform which are not maintained within the ADVANCE project, therefore should not be taken into account within this deliverable.		The ADVANCE D3.2 deliverable is composed of the present document and the Rodin toolset. The considered Rodin toolset consits of the Rodin core platform and the plug-ins created or maintained in the frame of the ADVANCE project. Indeed, there are contributed plug-ins available for the Rodin core platform which are not maintained within the ADVANCE project, therefore should not be taken into account within this deliverable.

	The Rodin platform can be downloaded from the SourceForge site ([http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/]). Moreover, the platform includes a collaborative documentation that is collected from two maintained locations :		The Rodin platform can be downloaded from the SourceForge site<ref>http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/</ref>. Moreover, the platform includes a collaborative documentation that is collected from two maintained locations :
	* the Event-B wiki <ref name="EventB_wiki">http://wiki.event-b.org</ref>,		* the Event-B wiki<ref name="EventB_wiki">http://wiki.event-b.org</ref>,
	* the Rodin Handbook <ref name="Rodin_handbook_Page">http://handbook.event-b.org</ref>.		* the Rodin Handbook<ref name="Rodin_handbook_Page">http://handbook.event-b.org</ref>.
	These locations can be consulted from outside the Rodin tool.		These locations can be consulted from outside the Rodin tool.

imported>Tommy at 10:23, 21 June 2012

2012-06-21T10:23:44Z

← Older revision		Revision as of 10:23, 21 June 2012
Line 1:		Line 1:
	The ADVANCE D3.2 deliverable is composed of the present document and the Rodin toolset. The Rodin toolset ~~considered is built~~ of the Rodin core platform and the plug-ins created or maintained in the frame of the ADVANCE project. Indeed, there are contributed plug-ins ~~that are~~ available for the Rodin core platform which are not maintained ~~in the frame of~~ the ADVANCE project, therefore should not be ~~considered~~ within this deliverable.		The ADVANCE D3.2 deliverable is composed of the present document and the Rodin toolset. The considered Rodin toolset consits of the Rodin core platform and the plug-ins created or maintained in the frame of the ADVANCE project. Indeed, there are contributed plug-ins available for the Rodin core platform which are not maintained within the ADVANCE project, therefore should not be taken into account within this deliverable.

	The Rodin platform can be downloaded from the SourceForge site ([http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/]). ~~The~~ platform includes a collaborative documentation that is collected from two maintained locations :		The Rodin platform can be downloaded from the SourceForge site ([http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/]). Moreover, the platform includes a collaborative documentation that is collected from two maintained locations :
	* the Event-B wiki <ref name="EventB_wiki">http://wiki.event-b.org</ref>,		* the Event-B wiki <ref name="EventB_wiki">http://wiki.event-b.org</ref>,
	* the Rodin Handbook <ref name="Rodin_handbook_Page">http://handbook.event-b.org</ref>.		* the Rodin Handbook <ref name="Rodin_handbook_Page">http://handbook.event-b.org</ref>.
			These locations can be consulted from outside the Rodin tool.

	The present document intends to ~~gives~~ a significant overview the work achieved within the WP3 ''Tooling research and development'' work package, during the first ten months of the ADVANCE project (Oct 2011 - Jul 2011), and aims to let the reader get a glimpse of the WP3 member's contribution plans and objectives.		The present document intends to give a significant overview of the work achieved within the WP3 ''Tooling research and development'' work package, during the first ten months of the ADVANCE project (Oct 2011 - Jul 2011), and aims to let the reader get a glimpse of the WP3 member's contribution plans and objectives.

	It is worth to remind that the ADVANCE project time frame overlaped with... blablabla {{TODO: Continue after lunch}}		It is worth to remind that the ADVANCE project time frame overlaped with... blablabla {{TODO: Continue after lunch}}