Difference between revisions of "User:Nicolas/Collections/ADVANCE D3.4 Introduction"

From Event-B
Jump to navigationJump to search
imported>Nicolas
(D3.4 Introduction, initial revision)
(No difference)

Revision as of 13:48, 6 October 2014

The ADVANCE D3.4 deliverable is composed of the present document and new extensions to the Rodin toolset as of November 2014. The considered Rodin toolset consists of the Rodin core platform and the plug-ins created or maintained in the frame of the ADVANCE project: ProB, UML-B, ProR, Camille, Theory, Composition, SMT. Other plug-ins, available for the Rodin platform but not maintained within the ADVANCE project, are not 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 third period of the ADVANCE project (Oct 2013 - Nov 2014), and aims to let the reader understand the WP3 member's contribution plans and objectives.

The document is divided according to the work package tasks: general platform maintenance, improvement of automated proof, model checking, language extension, model composition and decomposition.

The common structure which is used for each contribution is the following:

  • 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 reported.
  • Available documentation. Some pointers to the available documentation or related publications are listed.
  • Conclusion. A brief summary about what has been achieved in the topic, and an overview of potential continuations.

References