ADVANCE D3.3 Revised 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.
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. 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.
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, 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
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. 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 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. 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 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
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.
