D45 Introduction

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

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

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

By the end of the third year of the DEPLOY 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 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 all DEPLOY partner listed issues.

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

• An increased usability and performance were the main targets in the scalability fulfilled improvements. They have been obtained throught major core and UI refactorings. Additional scalability was gained with the addition of the Generic Instantiation Plug-in (previously mentionned as Design Pattern Managmement).
• A Model 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 parameterizable tactic profiles.

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

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 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.