D32 Introduction
The DEPLOY's D32 deliverable is composed of:
- The Rodin core platform and plug-ins (i.e. the DEPLOY tools).
- This document.
The Rodin platform can be downloaded from SourceForge site ([1]). The tool documentation is provided within the Event-B wiki ([2]).
This document gives an insight into the work achieved throughout the WP9 Tooling research and development work package, during the third year of the DEPLOY project (Feb 2010-Jan 2011), and depicts the WP9 partner's objectives for the coming year.
Among the aims that WP9 partners reached, it might be worth to cite : TODO Refactor this part.
- Improved scalability of the Rodin platform to support industrial deployments, through GUI enhancements (smart completion, renaming, text editing, etc), decomposition support and design-pattern management.
- Prover integrity and performance, to enhance the confidence in provers and to enlarge their proving capabilities. To this aim, the existing provers have been improved and a new rule-based prover plug-in has been implemented.
- Model animation and testing, to validate Event-B models. More precisely, the ProB or AnimB plug-ins allow a domain expert to detect errors in a model and ensure the presence of desired functionalities. Moreover, it is very important for many industrial applications to be able to completely hide the underlying formal specification.
- Model checking (ProB), to enable users to find sequences of events that prevent safety properties or proof obligations to be fulfilled.
- UML integration. UML-B provides a diagrammatic, formal modelling notation based on UML.
- Code generation, to enable complete support for development, from high-level Event-B models down to executable implementations. An initial definition of language support for code generation has been put forward.
The various parts making up this document are the following: general platform maintenance, mathematical extensions, provers, UML-B improvements, code generation, teamwork, scalability, model animation, and model-based testing.
Note that each of these parts is describing the improvements made, and is structured as follows:
- Overview. The involved partners are identified and an overview of the contribution is given.
- Motivations. The motivations for each tool extension and improvement are expressed.
- Choices / decisions. The decisions (e.g. design decisions) are justified.
- Available documentation. Some pointers to the Event-B wiki or related publications are listed.
- Planning. A timeline and the current status (as of 28 Jan 2011) is given.
