About Deploy Project
Tooling research and development
Robust tools are a vital ingredient for the successful deployment of formal methods in industry.
Building upon the tool-base provided by the RODIN project, WP9 will undertake research and development
of tools, with two major objectives:
- to ensure that the tools can be applied dependably and effectively to large-scale industrial projects.
Two major challenges are the scalability of the tools, which should be able to handle industrial size
models, and the ease of use and increased productivity in an industrial context.
- to extend the functionality of the tools for the new methods developed in WP6-WP8 as well as for specific needs
identified by the industrial partners. This will usually require the development of new techniques and algorithms
which will materialize as new plugins are integrated into the existing platform provided by the RODIN project.
These developments will also help integrate our formal engineering tools into the current development practice
of the industrial partners.
The research and development of the Tooling R&D workpackage is thus guided very specifically by industrial deployment;
many of the tasks and deliverables have been explicitly identified by the DEPLOY industrial partners during the proposal
preparation phase in order to obtain increased productivity and dependability.
The tasks of the Tooling R&D workpackage are grouped according to the following two objectives:
- Model Construction and Management tools (tasks T9.1 to T9.4). The objective of these tasks is to enhance
the tools platform in order to enable productive model construction and requirements management at an industrial level.
The work will focus on supporting the management and traceability of requirements (T9.1), combining UML with Event-B (T9.2),
improving the scalability of the tool platform (T9.3) and supporting extension of the mathematical language (T9.4).
- Model Analysis Tools (tasks T9.5 to T9.8). Mechanical verification and validation of models are at the heart
of the DEPLOY approach. The objective of these tasks is to develop tools for verifying and validating large,
industrial-sized formal models by means of powerful proof techniques, animation, testing and systematic model checking.
Task T9.5 focuses on model animation and testing. Task T9.6 works on model checking tools. Task T9.7 will improve the
prover performance. Task T9.8 will address specifically the integrity of the proof tools.
Organization and scheduling
It would not be conceivable to start such ambitious work from scratch, and we have the good fortune to benefit from the
excellent work done in the RODIN project which led to an open platform and a series of prototype plugins. All of the tool
development work undertaken in WP9 will build on the existing Eclipse-based platform developed by the RODIN project.
The open Eclipse platform is already well-supported and used in industry which means that our efforts will benefit a large
industrial community. The base provided by RODIN will permit us to focus our work on designing industrial strength tools.
During DEPLOY's lifetime, we will consider further tooling improvements and extensions, if the need is expressed by the industrial
partners or arises from the methodology research. The re-focus point planned at M19 will allow the DEPLOY partners to refine the tooling
objectives and to define a new effort distribution. The re-focus point will allow WP9 to take into account the industrial requirements
that will undoubtedly emerge during the pilot deployments of formal methods in WP1-WP4. The re-focus point will also serve as milestones
to evaluate the appropriateness of the technical choices made regarding the adequacy between final tools and industrial requirements
(e.g., scalability). In order to remain grounded in industrial needs, early versions of tools will be field-tested by the industrial
partners when deploying formal methods in WP1 to WP4.