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 tasks that the WP9 partners were committed to achieve and are worth citing:

The various parts making up this document are the following: 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.