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