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 and last year of DEPLOY.

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.