ADVANCE D3.3 Revised Roadmap - Revision history

imported>Laurent at 16:41, 2 December 2013

2013-12-02T16:41:02Z

← Older revision		Revision as of 16:41, 2 December 2013
Line 9:		Line 9:
	On the other hand, partners request better support for proving with theories. The available tactics provided are not sufficient, and the integration with external provers is not yet satisfactory. Focus will be given to enhancements on these aspects which will accompany the consolidation work.		On the other hand, partners request better support for proving with theories. The available tactics provided are not sufficient, and the integration with external provers is not yet satisfactory. Focus will be given to enhancements on these aspects which will accompany the consolidation work.

	While the complexity of case study models increased in line with to their size, the ratio of automatically discharged proof obligations decreased. Often, the application of small manual proof steps suffices to let the existing proving tools discharge the proof obligations. This situation although already encountered in previous projects involving the Rodin toolset shows that the addition of new tactics, and enhancement of the existing proof tooling is a continuous duty which has to be carried on until the end of the ADVANCE project. Note that this issue will also be partially addressed by the planned work of integrating the Super Zenon theorem prover.		While the complexity of case study models increased in line with their size, the ratio of automatically discharged proof obligations decreased. Often, the application of small manual proof steps suffices to let the existing proving tools discharge the proof obligations. This situation although already encountered in previous projects involving the Rodin toolset shows that the addition of new tactics, and enhancement of the existing proof tooling is a continuous duty which has to be carried on until the end of the ADVANCE project. Note that this issue will also be partially addressed by the planned work of integrating the Super Zenon theorem prover.

	Finally, customised animation of high-level models appeared to be a major requirement from the industrial partners. Indeed, it is a priority task to get a domain-specific point of view on high-level Event-B models and be able to validate their behaviour using the animation. Support for this is already provided by ProB and BMotion Studio ~~bug~~ further enhancements directed by feedback from case study work will take place by the end of the project.		Finally, customised animation of high-level models appeared to be a major requirement from the industrial partners. Indeed, it is a priority task to get a domain-specific point of view on high-level Event-B models and be able to validate their behaviour using the animation. Support for this is already provided by ProB and BMotion Studio but further enhancements directed by feedback from case study work will take place by the end of the project.

	== Work package specific needs ==		== Work package specific needs ==

	~~Partners of~~ WP1 expressed specific tooling needs on the following aspects : decomposition, testing, visualisation, and in linking the STPA method with Event-B and system developement lifecycle.		The WP1 partners expressed specific tooling needs on the following aspects : decomposition, testing, visualisation, and in linking the STPA method with Event-B and system developement lifecycle.
	WP2 partners expressed tooling needs according to the phased evolution of their work.		The WP2 partners expressed tooling needs according to the phased evolution of their work.
	In the first phase, they are in need of support for composition. In the second phase, they will need support for multi-simulation, test-case generation, and code generation.		In the first phase, they are in need of support for composition. In the second phase, they will need support for multi-simulation, test-case generation, and code generation.

Line 24:		Line 24:
	Help and improvements on composition and decomposition will then be provided to WP1 and WP2 according to their feedback on existing tooling limitations : in particular the ability to compose refinements and not just abstract models.		Help and improvements on composition and decomposition will then be provided to WP1 and WP2 according to their feedback on existing tooling limitations : in particular the ability to compose refinements and not just abstract models.

	The other tasks concerning testing, visualisation, and linking Event-B with STPA and system development lifecycle ~~are related to work package 4~~. However, they may ~~imply~~ some ~~evolutions from~~ the modelling and proof ~~tooling support. Priority will be given~~ to ~~such needs and enhancements of the Rodin platform will~~ be performed by WP3 ~~partners~~.		The other tasks concerning testing, visualisation, and linking Event-B with STPA and system development lifecycle will be carried out in WP4. However, they may require some evolution of the modelling and proof tools to be performed within WP3.

	== Conclusion ==		== Conclusion ==

imported>Tommy at 16:07, 2 December 2013

2013-12-02T16:07:27Z

imported>Tommy: Tommy moved page ADVANCE Deliverable D3.3 Revised Roadmap to ADVANCE D3.3 Revised Roadmap without leaving a redirect: Fectch section naming format which was used in other parts of the deliverable.

2013-11-29T17:52:11Z

Tommy moved page ADVANCE Deliverable D3.3 Revised Roadmap to ADVANCE D3.3 Revised Roadmap without leaving a redirect: Fectch section naming format which was used in other parts of the deliverable.

← Older revision	Revision as of 17:52, 29 November 2013
(No difference)

imported>Laurent at 17:31, 29 November 2013

2013-11-29T17:31:13Z

imported>Tommy: /* Conclusion */

2013-11-29T16:22:36Z

Conclusion

← Older revision		Revision as of 16:22, 29 November 2013
Line 29:		Line 29:

	As seen in this section, priority will be given to tasks needed by case studies to reach success.		As seen in this section, priority will be given to tasks needed by case studies to reach success.
	~~The~~ other tasks which are planned and which appear in the roadmap of D3.1 will be performed ~~depending on~~ the remaining resources available once the above prioritized tasks are fulfilled.		Thus, the other tasks which are planned and which appear in the roadmap of D3.1 will be performed in consideration of the remaining resources available once the above prioritized tasks are fulfilled.

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

imported>Tommy at 16:21, 29 November 2013

2013-11-29T16:21:22Z

← Older revision		Revision as of 16:21, 29 November 2013
Line 28:		Line 28:
	== Conclusion ==		== Conclusion ==

	As seen, priority will be given to tasks needed ~~for~~ case studies to reach success.		As seen in this section, priority will be given to tasks needed by case studies to reach success.
	The other tasks which are planned and which appear in the roadmap of D3.1 will be performed depending on the remaining resources available once the above prioritized tasks are fulfilled.		The other tasks which are planned and which appear in the roadmap of D3.1 will be performed depending on the remaining resources available once the above prioritized tasks are fulfilled.
	~~== References ==~~
	~~<references/>~~

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

imported>Tommy: /* Work package specific needs */

2013-11-29T16:20:33Z

Work package specific needs

← Older revision		Revision as of 16:20, 29 November 2013
Line 24:		Line 24:
	Help and improvements on composition and decomposition will then be provided to WP1 and WP2 according to their feedback on existing tooling limitations.		Help and improvements on composition and decomposition will then be provided to WP1 and WP2 according to their feedback on existing tooling limitations.

	The other tasks mentionned above are related to work package four, but may need some evolutions from the modelling and proof tooling support. Priority will be given on such needs and enancements of the Rodin platform will be performed by WP3 partners.		The other tasks mentionned above are related to work package four, but may need some evolutions from the modelling and proof tooling support. Priority will be given to such needs and enancements of the Rodin platform will be performed by WP3 partners.

	== Conclusion ==		== Conclusion ==

imported>Tommy: /* Work package specific needs */

2013-11-29T16:19:43Z

Work package specific needs

← Older revision		Revision as of 16:19, 29 November 2013
Line 21:		Line 21:
	WP1 case study models represent a large-scale system involving heterogeneous actors and which interfaces with a rich environment. When refining the abstract model, it appears that several entities can be decomposed. A seamless support of modifications within decomposed modelling artifacts is needed. Some work guided by WP1 feedback on decomposition limitations will be carried on.		WP1 case study models represent a large-scale system involving heterogeneous actors and which interfaces with a rich environment. When refining the abstract model, it appears that several entities can be decomposed. A seamless support of modifications within decomposed modelling artifacts is needed. Some work guided by WP1 feedback on decomposition limitations will be carried on.

	The WP2 case study tackles a massively distributed system where several identical entities can be recomposed to ~~form~~ the global system.		The WP2 case study tackles a massively distributed system where several identical entities can be recomposed to represent the global system.
	Help and improvements on composition and decomposition will then be provided to WP1 and WP2 according to their feedback on existing tooling limitations.		Help and improvements on composition and decomposition will then be provided to WP1 and WP2 according to their feedback on existing tooling limitations.

imported>Tommy: /* Work package specific needs */

2013-11-29T16:19:05Z

Work package specific needs

← Older revision		Revision as of 16:19, 29 November 2013
Line 19:		Line 19:
	In a first time, they are in need of support for composition. In a second time, they will need support for multi-simulation, test-case generation, and code generation.		In a first time, they are in need of support for composition. In a second time, they will need support for multi-simulation, test-case generation, and code generation.

	WP1 case study models represent a large-scale system which interfaces with a rich environment. When refining the abstract model, it appears that several entities can be decomposed. A seamless support of modifications within decomposed modelling artifacts is needed. Some work guided by WP1 feedback on decomposition limitations will be carried on.		WP1 case study models represent a large-scale system involving heterogeneous actors and which interfaces with a rich environment. When refining the abstract model, it appears that several entities can be decomposed. A seamless support of modifications within decomposed modelling artifacts is needed. Some work guided by WP1 feedback on decomposition limitations will be carried on.

	The WP2 case study tackles a massively distributed system where several identical entities can be recomposed to form the global system.		The WP2 case study tackles a massively distributed system where several identical entities can be recomposed to form the global system.

imported>Tommy: /* Work package specific needs */

2013-11-29T16:18:25Z

Work package specific needs

← Older revision		Revision as of 16:18, 29 November 2013
Line 20:		Line 20:

	WP1 case study models represent a large-scale system which interfaces with a rich environment. When refining the abstract model, it appears that several entities can be decomposed. A seamless support of modifications within decomposed modelling artifacts is needed. Some work guided by WP1 feedback on decomposition limitations will be carried on.		WP1 case study models represent a large-scale system which interfaces with a rich environment. When refining the abstract model, it appears that several entities can be decomposed. A seamless support of modifications within decomposed modelling artifacts is needed. Some work guided by WP1 feedback on decomposition limitations will be carried on.

	The WP2 case study tackles a massively distributed system where several identical entities can be recomposed to form the global system.		The WP2 case study tackles a massively distributed system where several identical entities can be recomposed to form the global system.
	Help and improvements on composition and decomposition will then be provided to WP1 and WP2 according to their feedback on existing tooling limitations.		Help and improvements on composition and decomposition will then be provided to WP1 and WP2 according to their feedback on existing tooling limitations.

← Older revision		Revision as of 16:07, 2 December 2013
Line 1:		Line 1:
	This section describes the needs of the industrial case studies (WP1 and WP2) which justify the further described revision of the tooling roadmap.		This section describes the needs of the industrial case studies (WP1 and WP2) which justify the further described revision of the tooling roadmap.

	During the ADVANCE plenary meeting which was held in Winchester November 7th and 8th, the industrial partners which are involved in work packages 1 and 2 expressed their tooling needs to support the case studies. Consequently, ADVANCE partners then agreed to revise together the roadmap which appears in the deliverable D3.1 by giving priority to the tasks addressing these needs by the end of the project.		During the ADVANCE plenary meeting which was held in Winchester November 7th and 8th, 2013 the industrial partners which are involved in work packages 1 and 2 expressed their tooling needs to support the case studies. Consequently, ADVANCE partners then agreed to revise together the roadmap which appears in the deliverable D3.1 by giving priority to the tasks already identified in D3.1 and addressing these needs by the end of the project.

	== Common needs across both work packages ==		== Common needs across both work packages ==

	For both WP1 and WP2 case studies, the need ~~of a~~ better support of theories, better automatic proving capability and customised model animation was expressed.		For both WP1 and WP2 case studies, the need for better support of theories, better automatic proving capability and customised model animation was expressed.
	As concerns the support of theories, two difficulties are met. On the first hand, the rapid evolution of the theory plug-in led to major refactorings of its code which affected its stability. Consolidation is needed and will be performed during the last period of the project to ensure the seamless integration of the plug-in within the Rodin platform.		As concerns the support of theories, two difficulties are met. On the first hand, the rapid evolution of the theory plug-in led to major refactorings of its code which affected its stability. Consolidation is needed and will be performed during the last period of the project to ensure the seamless integration of the plug-in within the Rodin platform.
	On the other hand, partners ~~are in need of a~~ better support for proving with theories. The available tactics provided are not sufficient, and the integration with external provers is not yet satisfactory. Focus will be given to enhancements on these aspects which will accompany the consolidation work.		On the other hand, partners request better support for proving with theories. The available tactics provided are not sufficient, and the integration with external provers is not yet satisfactory. Focus will be given to enhancements on these aspects which will accompany the consolidation work.

	While the complexity of case study models increased ~~concurrently~~ to their size, the ratio of automatically discharged proof obligations decreased. Often, the application of small manual proof steps suffices to let the existing proving tools discharge the proof obligations. This situation although already encountered in previous projects involving the Rodin toolset shows that the addition of new tactics, and enhancement of the existing proof tooling is a continuous duty which has to be carried on until the end of the ADVANCE project. Note that this issue will also be partially addressed by the planned work of integrating the Super Zenon theorem prover.		While the complexity of case study models increased in line with to their size, the ratio of automatically discharged proof obligations decreased. Often, the application of small manual proof steps suffices to let the existing proving tools discharge the proof obligations. This situation although already encountered in previous projects involving the Rodin toolset shows that the addition of new tactics, and enhancement of the existing proof tooling is a continuous duty which has to be carried on until the end of the ADVANCE project. Note that this issue will also be partially addressed by the planned work of integrating the Super Zenon theorem prover.

	Finally, customised animation of high-level models appeared to be a major ~~concern to~~ industrial partners. Indeed, it is a priority task to get a domain-specific point of view on high-level Event-B models and be able to validate their behaviour using the animation. ~~Some~~ enhancements directed by feedback from case study work will take place by the end of the project.		Finally, customised animation of high-level models appeared to be a major requirement from the industrial partners. Indeed, it is a priority task to get a domain-specific point of view on high-level Event-B models and be able to validate their behaviour using the animation. Support for this is already provided by ProB and BMotion Studio bug further enhancements directed by feedback from case study work will take place by the end of the project.

	== Work package specific needs ==		== Work package specific needs ==

	Partners of WP1 expressed specific tooling needs on the following aspects : decomposition, testing, visualisation, and in linking the STPA method with Event-B and system developement lifecycle.		Partners of WP1 expressed specific tooling needs on the following aspects : decomposition, testing, visualisation, and in linking the STPA method with Event-B and system developement lifecycle.
	WP2 partners expressed tooling needs according to the evolution of their work.		WP2 partners expressed tooling needs according to the phased evolution of their work.
	In a first ~~time~~, they are in need of support for composition. In a second ~~time~~, they will need support for multi-simulation, test-case generation, and code generation.		In the first phase, they are in need of support for composition. In the second phase, they will need support for multi-simulation, test-case generation, and code generation.

	WP1 case study models represent a large-scale system involving heterogeneous actors and which interfaces with a rich environment. When refining the abstract model, it appears that several entities can be decomposed. A seamless support of modifications within decomposed modelling artifacts is needed. Some work guided by WP1 feedback on decomposition limitations will be carried on.		The WP1 case study models represent a large-scale system involving heterogeneous actors and which interfaces with a rich environment. When refining the abstract model, it appears that several entities can be decomposed. A seamless support of modifications within decomposed modelling artifacts is needed. Some work guided by WP1 feedback on decomposition limitations will be carried on.

	The WP2 case study tackles a ~~massively~~ distributed system where several identical entities can be recomposed to represent the global system.		The WP2 case study tackles a distributed system where several identical entities can be recomposed to represent the global system.
	Help and improvements on composition and decomposition will then be provided to WP1 and WP2 according to their feedback on existing tooling limitations.		Help and improvements on composition and decomposition will then be provided to WP1 and WP2 according to their feedback on existing tooling limitations : in particular the ability to compose refinements and not just abstract models.

	The other tasks ~~mentioned above~~ are related to work package 4, ~~but~~ may ~~need~~ some evolutions from the modelling and proof tooling support. Priority will be given to such needs and enhancements of the Rodin platform will be performed by WP3 partners.		The other tasks concerning testing, visualisation, and linking Event-B with STPA and system development lifecycle are related to work package 4. However, they may imply some evolutions from the modelling and proof tooling support. Priority will be given to such needs and enhancements of the Rodin platform will be performed by WP3 partners.

	== Conclusion ==		== Conclusion ==

← Older revision		Revision as of 17:31, 29 November 2013
Line 1:		Line 1:
	This section ~~aims to give some feedback on~~ industrial case ~~study needs~~ which justify the further described revision of the tooling roadmap.		This section describes the needs of the industrial case studies (WP1 and WP2) which justify the further described revision of the tooling roadmap.

	During the ADVANCE plenary meeting ~~that~~ held in Winchester ~~on november~~ 7th and 8th, the industrial partners which are involved in work packages ~~one~~ and ~~two~~ expressed their needs ~~in tooling~~ to support the case studies. Consequently, ADVANCE partners then agreed to revise together the roadmap which appears in the deliverable D3.1 by giving priority to the tasks addressing these needs by the end of the project.		During the ADVANCE plenary meeting which was held in Winchester November 7th and 8th, the industrial partners which are involved in work packages 1 and 2 expressed their tooling needs to support the case studies. Consequently, ADVANCE partners then agreed to revise together the roadmap which appears in the deliverable D3.1 by giving priority to the tasks addressing these needs by the end of the project.

	== Common needs ~~accross~~ both work packages ==		== Common needs across both work packages ==

	For both WP1 and WP2 case studies, the need of a better support of theories, better automatic proving capability and ~~tailored~~ model animation was expressed.		For both WP1 and WP2 case studies, the need of a better support of theories, better automatic proving capability and customised model animation was expressed.
	As concerns the support of theories, two difficulties are met. On the first hand, the rapid evolution of the theory plug-in led to major refactorings of its code which affected its stability. Consolidation is needed and will be performed during the last period of the project to ensure the seamless integration of the plug-in within the Rodin platform.		As concerns the support of theories, two difficulties are met. On the first hand, the rapid evolution of the theory plug-in led to major refactorings of its code which affected its stability. Consolidation is needed and will be performed during the last period of the project to ensure the seamless integration of the plug-in within the Rodin platform.
	On the other hand, partners are in need of a better support for proving with theories. The available tactics provided are not sufficient, and the integration with external provers is not yet satisfactory. Focus will be given to enhancements on these aspects which will accompany the consolidation work.		On the other hand, partners are in need of a better support for proving with theories. The available tactics provided are not sufficient, and the integration with external provers is not yet satisfactory. Focus will be given to enhancements on these aspects which will accompany the consolidation work.
Line 11:		Line 11:
	While the complexity of case study models increased concurrently to their size, the ratio of automatically discharged proof obligations decreased. Often, the application of small manual proof steps suffices to let the existing proving tools discharge the proof obligations. This situation although already encountered in previous projects involving the Rodin toolset shows that the addition of new tactics, and enhancement of the existing proof tooling is a continuous duty which has to be carried on until the end of the ADVANCE project. Note that this issue will also be partially addressed by the planned work of integrating the Super Zenon theorem prover.		While the complexity of case study models increased concurrently to their size, the ratio of automatically discharged proof obligations decreased. Often, the application of small manual proof steps suffices to let the existing proving tools discharge the proof obligations. This situation although already encountered in previous projects involving the Rodin toolset shows that the addition of new tactics, and enhancement of the existing proof tooling is a continuous duty which has to be carried on until the end of the ADVANCE project. Note that this issue will also be partially addressed by the planned work of integrating the Super Zenon theorem prover.

	Finally, ~~tailored~~ animation of high-level models appeared to be a major concern to industrial partners. Indeed, it is a ~~prior~~ task to get a domain-specific point of view on high-level Event-B models and be able to validate their behaviour using the animation. Some enhancements directed by feedback from case study work will take place by the end of the project.		Finally, customised animation of high-level models appeared to be a major concern to industrial partners. Indeed, it is a priority task to get a domain-specific point of view on high-level Event-B models and be able to validate their behaviour using the animation. Some enhancements directed by feedback from case study work will take place by the end of the project.

	== Work package specific needs ==		== Work package specific needs ==
Line 24:		Line 24:
	Help and improvements on composition and decomposition will then be provided to WP1 and WP2 according to their feedback on existing tooling limitations.		Help and improvements on composition and decomposition will then be provided to WP1 and WP2 according to their feedback on existing tooling limitations.

	The other tasks ~~mentionned~~ above are related to work package ~~four~~, but may need some evolutions from the modelling and proof tooling support. Priority will be given to such needs and ~~enancements~~ of the Rodin platform will be performed by WP3 partners.		The other tasks mentioned above are related to work package 4, but may need some evolutions from the modelling and proof tooling support. Priority will be given to such needs and enhancements of the Rodin platform will be performed by WP3 partners.

	== Conclusion ==		== Conclusion ==

	As seen in this section, priority will be given to tasks needed by case studies ~~to reach success~~.		As seen in this section, priority will be given to the tasks needed to complete successfully the case studies.
	Thus, the other tasks which are planned and which appear in the roadmap of D3.1 will be performed in consideration of the remaining resources available once the above prioritized tasks ~~are fulfilled~~.		Thus, the other tasks which are planned and which appear in the roadmap of D3.1 will be performed in consideration of the remaining resources available once the above prioritized tasks have been completed.

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