D45 Introduction

The DEPLOY deliverable D45 is made of this document, the Rodin core platform, and its plug-ins (i.e. the DEPLOY tools). The Rodin platform can be retrieved from the SourceForge site. The documentation of the DEPLOY tools is available from two sites:

• the Event-B wiki.
• the Event-B Handbook.

This document gives an overview of the work done within the WP9 Tooling research and development work package, during the fourth and last period of the DEPLOY project (Feb 2011-Apr 2012). It also gives a status of the toolset by the end of the DEPLOY project.

At the end of the third year of the project, the DEPLOY industrial partners reported some issues they encountered and expressed some specific requests which were then considered mandatory to be addressed before the end of the DEPLOY project. Hence, the various tasks to be done by the WP9 partners have been early scheduled, prioritized, and periodically updated to both fit with the original Description of Work (DoW) and give answers to DEPLOY partner issues.

Here is a short list of important results that WP9 partners committed to achieve and are worth citing in this introduction:

• Increasing usability and performance of the toolset was the main targets regarding scalability. They have been obtained through major core and UI refactorings. More scalability was gained with the addition of the Generic Instantiation Plug-in (previously mentioned as Design Pattern Management).
• A Model-Based Testing plug-in whose development was guided by the needs of WP1-4 partners has been released and documented.
• Increasing prover performance through the addition of several rewriting or inference rules, as well as two plug-ins, the Export to Isabelle and SMT Solvers which both help to raise the number of automatically discharged proof obligations.
• An enhanced proving experience, and proving ability with the introduction of user customizable and parametrizable tactic profiles.

This document is made of the following parts: general platform maintenance, scalability, prover enhancement, code generation, model-based testing, and model-checking.

Note that each of these parts describes the improvements performed, and is structured, except the general platform maintenance part, as follows:

• Overview. The involved partners are identified and an overview of the contribution is given.
• Motivations. The motivations for each improvement are expressed.
• Choices / decisions. The decisions (e.g. design decisions) are justified.
• Available documentation. Some pointers to the Event-B wiki, handbook, or related publications are listed.
• Status. The status reached on the given topic at the end of the Deploy project (as of 30 Apr 2012) is given.
• References. The references for further details.

This structure has been chosen, as in the previous tooling deliverables (D23, D32), in order to highlight the answers given to each tasks mentioned in the Description of Work (DoW). The first part being focused on tool maintenance is structured upon the same template but for each considered plug-in, in order to ease the reading.