Difference between revisions of "ADVANCE D3.2 Introduction"

From Event-B
Jump to navigationJump to search
imported>Tommy
m
imported>Tommy
m
Line 12: Line 12:
 
The document is divided into four parts: general platform maintenance, improvement of automated proof, language extension, model checking, and model composition and decomposition.
 
The document is divided into four parts: general platform maintenance, improvement of automated proof, language extension, model checking, and model composition and decomposition.
  
Note that each of these parts is describing the improvements made, and is structured as follows:
+
The common structure that is reuse for each contribution in the general platform maintenance part and later, in the other part could be detailed as follows:
 
* Overview. The involved partners are identified and an overview of the contribution is given.
 
* Overview. The involved partners are identified and an overview of the contribution is given.
 
* Motivations / Decisions. The motivation for each tool extension and improvement are expressed. The decisions (e.g. design decision) are related.
 
* Motivations / Decisions. The motivation for each tool extension and improvement are expressed. The decisions (e.g. design decision) are related.

Revision as of 12:55, 21 June 2012

The ADVANCE D3.2 deliverable is composed of the present document and the Rodin toolset. The considered Rodin toolset consits of the Rodin core platform and the plug-ins created or maintained in the frame of the ADVANCE project. Indeed, there are contributed plug-ins available for the Rodin core platform which are not maintained within the ADVANCE project, therefore should not be taken into account within this deliverable.

The Rodin platform can be downloaded from the SourceForge site[1].
Moreover, the platform includes a collaborative documentation that is collected from two maintained locations :

  • the Event-B wiki[2],
  • the Rodin Handbook[3].

These locations can be consulted from outside the Rodin tool.

The present document intends to give a relevant overview of the work achieved within the work package 3: Methods and Tools for Model Construction and Proof, during the first ten months of the ADVANCE project (Oct 2011 - Jul 2011), and aims to let the reader get a glimpse of the WP3 member's contribution plans and objectives. It is worth reminding that the ADVANCE project time frame overlapped the end of the EU FP7 DEPLOY project[4] from October 2011 to April 2012. Therefore, the commitment of WP3 members that were members of DEPLOY tooling workpackage as well, was mainly devoted during this period to consolidate the toolset by fixing the identified bugs and rectigying usability issues. These activities encompass the objectives of the task 3.2 mentionned in the ADVANCE Description of Work (DoW).

The document is divided into four parts: general platform maintenance, improvement of automated proof, language extension, model checking, and model composition and decomposition.

The common structure that is reuse for each contribution in the general platform maintenance part and later, in the other part could be detailed as follows:

  • Overview. The involved partners are identified and an overview of the contribution is given.
  • Motivations / Decisions. The motivation for each tool extension and improvement are expressed. The decisions (e.g. design decision) are related.
  • Available documentation. Some pointers to the available documentation or related publications are listed.
  • Planning. The current status about the topic (as of July 2012), and an overview of the future plans are given.

References