ADVANCE D3.3 Revised Roadmap: Difference between revisions

From Event-B
Jump to navigationJump to search
imported>Tommy
mNo edit summary
imported>Laurent
mNo edit summary
 
(15 intermediate revisions by 2 users not shown)
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 and give 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 accross both work packages ==
== Common needs across both work packages ==


For both workpage 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 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 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 led by work packages feedback 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 on the following aspects according to two periods by the end of the ADVANCE project.
The 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 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 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.


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 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 : 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 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 ==


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 the tasks needed to complete successfully the  case studies.
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 have been completed.
== References ==
<references/>


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

Latest revision as of 16:41, 2 December 2013

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, 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

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. 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 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 but further enhancements directed by feedback from case study work will take place by the end of the project.

Work package specific needs

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. 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.

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 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 : 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 will be carried out in WP4. However, they may require some evolution of the modelling and proof tools to be performed within WP3.

Conclusion

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 have been completed.