ADVANCE D3.3 Revised Roadmap

This section aims to give some feedback on industrial case study needs 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.

Common needs accross 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. 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, 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.

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

Conclusion

As seen, priority will be given to tasks needed for 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.