User:Nicolas/Collections/ADVANCE D3.4 General Platform Maintenance - Revision history

imported>Nicolas: /* Motivations / Decisions */ Advance -> ADVANCE

2014-11-25T09:54:15Z

Motivations / Decisions: Advance -> ADVANCE

← Older revision		Revision as of 09:54, 25 November 2014
Line 87:		Line 87:

	The ability to generate reports is important. For instance, it is desirable to see statistics (the number of requirements currently covered by the model) so that this can be presented to a customer during progress meetings.		The ability to generate reports is important. For instance, it is desirable to see statistics (the number of requirements currently covered by the model) so that this can be presented to a customer during progress meetings.
	In order to meet this goal, first experiments towards a reporting tool for ProR have been made during the ~~Advance~~ Project<ref name="prorreport" />.		In order to meet this goal, first experiments towards a reporting tool for ProR have been made during the ADVANCE Project<ref name="prorreport" />.

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

imported>Ladenberger: /* ProR/Rodin Integration Plugin */

2014-11-24T14:35:37Z

ProR/Rodin Integration Plugin

← Older revision		Revision as of 14:35, 24 November 2014
Line 76:		Line 76:
	A requirements Meta-Model for the WP-1 and WP-2 industrial case studies has been developed during the last period of the ADVANCE project.		A requirements Meta-Model for the WP-1 and WP-2 industrial case studies has been developed during the last period of the ADVANCE project.
	Moreover, several requested features were added. For instance, when the user selects a linked element (guard, invariant, etc.) in the requirements document, the tool takes the user directly to the corresponding element in the Event-B model.		Moreover, several requested features were added. For instance, when the user selects a linked element (guard, invariant, etc.) in the requirements document, the tool takes the user directly to the corresponding element in the Event-B model.
			First experiments have been made towards a feature to automatically generate reports from ProR<ref name="prorreport">http://www.stups.hhu.de/w/Reporting_f%C3%BCr_ReqIF:_Von_der_Analyse_bis_zur_Auswertung</ref>.
	Beside this, general improvements, such as usability improvements have been made on the ProR/Rodin integration plugin during the last period of the ADVANCE project.		Beside this, general improvements, such as usability improvements have been made on the ProR/Rodin integration plugin during the last period of the ADVANCE project.

Line 85:		Line 86:
	In order to improve the usability and the integration between the ProR tool and the Rodin platform, a new feature has been added to switch between the requirements document and the Event-B model. Whenever the user selects a linked element (guard, invariant, etc.) in the requirements document, the tool takes the user directly to the corresponding element in the Event-B model.		In order to improve the usability and the integration between the ProR tool and the Rodin platform, a new feature has been added to switch between the requirements document and the Event-B model. Whenever the user selects a linked element (guard, invariant, etc.) in the requirements document, the tool takes the user directly to the corresponding element in the Event-B model.

			The ability to generate reports is important. For instance, it is desirable to see statistics (the number of requirements currently covered by the model) so that this can be presented to a customer during progress meetings.
			In order to meet this goal, first experiments towards a reporting tool for ProR have been made during the Advance Project<ref name="prorreport" />.
	=== Available Documentation ===		=== Available Documentation ===

imported>Ladenberger: /* ProR/Rodin Integration Plugin */

2014-11-24T14:26:54Z

ProR/Rodin Integration Plugin

← Older revision		Revision as of 14:26, 24 November 2014
Line 75:		Line 75:

	A requirements Meta-Model for the WP-1 and WP-2 industrial case studies has been developed during the last period of the ADVANCE project.		A requirements Meta-Model for the WP-1 and WP-2 industrial case studies has been developed during the last period of the ADVANCE project.
			Moreover, several requested features were added. For instance, when the user selects a linked element (guard, invariant, etc.) in the requirements document, the tool takes the user directly to the corresponding element in the Event-B model.
	Beside this, general improvements, such as usability improvements have been made on the ProR/Rodin integration plugin during the last period of the ADVANCE project.		Beside this, general improvements, such as usability improvements have been made on the ProR/Rodin integration plugin during the last period of the ADVANCE project.

Line 81:		Line 82:
	The ProR/Rodin integration plugin provides a default Meta-Model for requirements documents. However, this Meta-Model does not support all specific needs and characteristics of the industrial case studies.		The ProR/Rodin integration plugin provides a default Meta-Model for requirements documents. However, this Meta-Model does not support all specific needs and characteristics of the industrial case studies.
	As a consequence, we decided to create a new requirements Meta-Model that supports the specific needs of both industrial case studies.		As a consequence, we decided to create a new requirements Meta-Model that supports the specific needs of both industrial case studies.

			In order to improve the usability and the integration between the ProR tool and the Rodin platform, a new feature has been added to switch between the requirements document and the Event-B model. Whenever the user selects a linked element (guard, invariant, etc.) in the requirements document, the tool takes the user directly to the corresponding element in the Event-B model.

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

imported>Colin: /* UML-B Improvements */

2014-11-24T13:13:28Z

UML-B Improvements

imported>Sebastian: /* Conclusion */

2014-11-20T14:09:14Z

Conclusion

← Older revision		Revision as of 14:09, 20 November 2014
Line 139:		Line 139:

	=== Conclusion ===		=== Conclusion ===
	Camille still has the drawback of not supporting extensibility. It only supports the core Event-B language and plug-in-specific additions are simply ignored. Consequently, users have to switch back to Rodin's native Editor to edit plug-in-specific modelling extensions. The changes and improvements to the development process performed in the last period should finally allow for a new and completely overhauled version of Camille to be implemented.		Camille still has the drawback of not supporting extensibility. It only supports the core Event-B language and plug-in-specific additions are simply ignored. Consequently, users have to switch back to Rodin's native Editor to edit plug-in-specific modelling extensions. However, Camille was extended in oder to preserve plug-in specific additions. This change allows switching between Camille and the other editors without loosing plugin specific information that Camille can not display. The changes and improvements to the development process performed in the last period should finally allow for a new and completely overhauled version of Camille to be implemented.

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

imported>Sebastian: /* Motivations / Decisions */

2014-11-20T14:06:14Z

Motivations / Decisions

← Older revision		Revision as of 14:06, 20 November 2014
Line 126:		Line 126:

	Camille's internal parser for the structure of Event-B machines and contexts has been split off of Camille and moved to ProB's general parsers library.		Camille's internal parser for the structure of Event-B machines and contexts has been split off of Camille and moved to ProB's general parsers library.
	~~This effectively renders~~ the parser ~~and external dependency for~~ Camille ~~and~~ further decouples core, ui and parsers.		Hence, the parser is now a completely separate project that can be developed independently of Camille.
			This further decouples Camille's core, ui and parsers.
	Externalising the parser is the first step to making Camille more modular in oder to be able to replace the parser by the upcoming block parser.		Externalising the parser is the first step to making Camille more modular in oder to be able to replace the parser by the upcoming block parser.
	In addition, externalising the parser makes it available for other projects as well.		In addition, externalising the parser makes it available for other projects as well.

imported>Sebastian: /* Conclusion */

2014-11-20T14:03:55Z

Conclusion

← Older revision		Revision as of 14:03, 20 November 2014
Line 138:		Line 138:

	=== Conclusion ===		=== Conclusion ===
	~~Sadly,~~ Camille still has the drawback of not supporting extensibility. It only supports the core Event-B language and plug-in-specific additions are simply ignored. Consequently, users have to switch back to Rodin's native Editor to edit plug-in-specific modelling extensions. The changes and improvements to the development process performed in the last period should finally allow for a new and completely overhauled version of Camille to be implemented.		Camille still has the drawback of not supporting extensibility. It only supports the core Event-B language and plug-in-specific additions are simply ignored. Consequently, users have to switch back to Rodin's native Editor to edit plug-in-specific modelling extensions. The changes and improvements to the development process performed in the last period should finally allow for a new and completely overhauled version of Camille to be implemented.

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

imported>Nicolas: /* Motivations / Decisions */

2014-11-19T13:30:41Z

Motivations / Decisions

← Older revision		Revision as of 13:30, 19 November 2014
Line 18:		Line 18:
	=== Motivations / Decisions ===		=== Motivations / Decisions ===

	The core API has been improved. In particular, the interface with the theory plug-in has been enriched so as to keep ~~trace~~ of language changes over time, thus enforcing model and proof consistency.		The core API has been improved. In particular, the interface with the theory plug-in has been enriched so as to keep track of language changes over time, thus enforcing model and proof consistency.

	New proof rules have been implemented (SIMP_EMPTY_PARTITION and SIMP_SINGLE_PARTITION).		New proof rules have been implemented (SIMP_EMPTY_PARTITION and SIMP_SINGLE_PARTITION).
Line 27:		Line 27:
	The underlying Eclipse Platform has been upgraded to the most recent version (Eclipse 4.4.1 as of Rodin 3.1). This was required by plug-in developers who wanted to take advantage of the newest Eclipse features. While also bringing fixes to some Eclipse bugs, it prepares for future developments based on the latest technology.		The underlying Eclipse Platform has been upgraded to the most recent version (Eclipse 4.4.1 as of Rodin 3.1). This was required by plug-in developers who wanted to take advantage of the newest Eclipse features. While also bringing fixes to some Eclipse bugs, it prepares for future developments based on the latest technology.

	For the same reasons, the code has been ported to Java 7, while remaining compatible with Java 1.6.		For the same reasons, the code has been ported to Java 7, while remaining compatible with Java 6.

	The source code is now distributed in a more developer-friendly format, so it's easier for plug-in implementers to extend Rodin as a target platform.		The source code is now distributed in a more developer-friendly format, so it's easier for plug-in implementers to extend Rodin as a target platform.

imported>Colin: /* Overview */

2014-11-07T16:32:43Z

Overview

← Older revision		Revision as of 16:32, 7 November 2014
Line 46:		Line 46:

	During the last period of Advance,		During the last period of Advance,
	* Classic UML-B has been migrated to Rodin 3.x. During this release some ~~improvemnts~~ and bug fixes were mode.		* Classic UML-B has been migrated to Rodin 3.x. During this release some improvements and bug fixes were mode.
	* iUML-B State-machines have undergone major structural improvements including a new Event-B generator ~~which~~ significantly improves performance. State-machine Animation has been integrated with ~~Bmotion~~ Studio so that both can be run in parallel.		* iUML-B State-machines have undergone major functional and structural improvements including new diagram features requested by users and a new Event-B generator that significantly improves performance. State-machine Animation has been integrated with BMotion Studio so that both can be run in parallel.
	* iUML-B Class diagrams have been released as a prototype and are under evaluation by industrial collaborators for use in their development process.		* iUML-B Class diagrams have been released as a prototype and are under evaluation by industrial collaborators for use in their development process.

imported>Colin: /* Available Documentation */

2014-11-07T16:30:49Z

Available Documentation

← Older revision		Revision as of 16:30, 7 November 2014
Line 60:		Line 60:

	=== Available Documentation ===		=== Available Documentation ===
	An overview and tutorial of both Classic UML-B and iUML-B can be found on the Event-B wiki.		An overview and tutorial of both Classic UML-B and iUML-B can be found on the Event-B wiki<ref>http://wiki.event-b.org/index.php/UML-B</ref>.

	=== Conclusion ===		=== Conclusion ===

← Older revision		Revision as of 13:13, 24 November 2014
Line 45:		Line 45:
	UML-B provides Class diagrams and State-machine diagrams for Event-B modelling. There are two versions of UML-B. The first, Classic UML-B, generates a complete Event-B project and all modelling is diagrammatic. The second, iUML-B, integrates diagrams inside Event-B machines and contexts and a mixture of diagrams and Event-B can be used in modelling.		UML-B provides Class diagrams and State-machine diagrams for Event-B modelling. There are two versions of UML-B. The first, Classic UML-B, generates a complete Event-B project and all modelling is diagrammatic. The second, iUML-B, integrates diagrams inside Event-B machines and contexts and a mixture of diagrams and Event-B can be used in modelling.

	During the last period of ~~Advance~~,		During the last period of ADVANCE,
	* Classic UML-B has been migrated to Rodin 3.x. During this release some improvements and bug fixes were ~~mode~~.		* Classic UML-B has been migrated to Rodin 3.x. During this release some improvements and bug fixes were made.
	* iUML-B State-machines have undergone major functional and structural improvements including new diagram features requested by users and a new Event-B generator that significantly improves performance. State-machine Animation has been integrated with BMotion Studio so that both can be run in parallel.		* iUML-B State-machines have undergone major functional and structural improvements including new diagram features requested by users (in particular, Critical Software in WP2) and a new Event-B generator that significantly improves performance. State-machine Animation has been integrated with BMotion Studio so that both can be run in parallel.
	* iUML-B Class diagrams have been released as a prototype and are under evaluation by industrial collaborators for use in their development process.		* iUML-B Class diagrams have been released as a prototype and are under evaluation by industrial collaborators for use in their development process.

Line 53:		Line 53:
	While Classic UML-B is still maintained and used by some industrial collaborators, most new development focusses on the more popular iUML-B.		While Classic UML-B is still maintained and used by some industrial collaborators, most new development focusses on the more popular iUML-B.

	The iUML-B ~~Statemachines~~ to Event-B translator was implemented in the QVTo declarative language. This suffered performance problems due to the need to recompile on each invocation. The translation was re-written using our own Java based generator framework which greatly improves performance.		The iUML-B Statemachine to Event-B translator was implemented in the QVTo declarative language. This suffered performance problems due to the need to recompile on each invocation. The translation was re-written using our own Java based generator framework which greatly improves performance.

	For valiation purposes users find visual animations very powerful and we have used both the State-machine animation and ~~BmotionStudio~~ in our collaborations with industry. However, previously, only one or the other could be launched at any particular time. A facility to also automatically launch any open ~~BmotionStudio~~ editor was added to the launch process of the state-machine editor. Both animations run from the same ProB animation instance. This provides an extremely strong visualisation of the model for validation purposes as the image representations of ~~Bmotion~~ Studio complement the ~~statemachine~~ visualisation and vice versa.		For valiation purposes users find visual animations very powerful and we have used both the State-machine animation and BMotionStudio in our collaborations with industry. However, previously, only one or the other could be launched at any particular time. A facility to also automatically launch any associated and open BMotionStudio editor was added to the launch process of the state-machine editor. Both animations run from the same ProB animation instance. This provides an extremely strong visualisation of the model for validation purposes as the image representations of BMotion Studio complement the state-machine visualisation and vice versa.

	The iUML-B class diagram plug-in was delayed as it was not the highest priority for ~~Advance~~ partners. However, other industrial users are interested in switching away from the Classic UML-B tool. A prototype release of iUML-B Class diagrams has now been made available to these industrial collaborators for evaluation purposes. A full release will be made by the end of 2014. During recent development of the plug-in, the mechanism for data elaboration has been rationalised and additional modelling features have been added which make the modelling tool more effective.		The iUML-B class diagram plug-in was delayed as it was not the highest priority for ADVANCE partners. However, other industrial users (e.g. Thales, Austria) are interested in switching away from the Classic UML-B tool. A prototype release of iUML-B Class diagrams has now been made available to these industrial collaborators for evaluation purposes. A full release will be made by the end of 2014. During recent development of the plug-in, the mechanism for data elaboration has been rationalised and additional modelling features have been added which make the modelling tool more effective.

	=== Available Documentation ===		=== Available Documentation ===
Line 63:		Line 63:

	=== Conclusion ===		=== Conclusion ===
	iUML-B state-machines and animation have been significantly improved throughout ~~Advance~~ and now represent a mature and popular tool.		iUML-B state-machines and animation have been significantly improved throughout ADVANCE and now represent a mature and popular tool.
	~~iUMl~~-B class diagrams promise to be equally successful as early indications are that the approach to data elaboration is effective.		iUML-B class diagrams promise to be equally successful as early indications are that the approach to data elaboration is effective.

	Classic UML-B will continued to be maintained but no new features are being added.		Classic UML-B will continued to be maintained but no new features are being added unless specifically requested by an industrial partner.

	== ProR/Rodin Integration Plugin ==		== ProR/Rodin Integration Plugin ==