D45 Introduction

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

• the Event-B wiki ([2]).
• the Event-B Handbook ([3]).

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 partners reported some issues they encountered and expressed some specific needs which were then considered mandatory to address 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 short list of important results that WP9 partners were committed to achieve and are worth citing in this introduction:

• Increased usability and performance were the main targets in the scalability fulfilled improvements. 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 which development was guided by the needs of WP1-4 partners has been released and documented,
• Increased 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 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 27 Apr 2012) is given.
• References. The references for further details.