Difference between pages "Rodin Plug-ins" and "User:Tommy/Collections/Deploy Deliverable D45"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Vitaly
 
imported>Tommy
 
Line 1: Line 1:
''For developer support, see [[Rodin Developer Support]]''
+
{{saved_book}}
 +
== Introduction ==
 +
The purpose of this page is to give a base for the final DEPLOY Deliverable D45 (Model Construction tools &  Analysis IV) which will be delivered to the European Commission (27 April 2012).
  
== Rodin Plug-in Documentation ==
+
== Template ==
 +
For each section covered in this document, a wiki page has been created and <b>shall be completed</b> (see [[#Contents | Contents]]). Each of them should give a brief description of the work that was carried on during the last year of the project (Feb 2011-April 2012 [Extension included]) within the WP9 package, without going deeply into technical details.<br>
 +
:<b>Goal: give to the project reviewers some insight which should look like an executive summary on a given WP9 topic.<br>
 +
:All details (papers, detailed wiki pages, etc.) should be made available as pointers.</b>
  
=== Modelling ===
+
This template provides a common structure for all of these pages.<br>
* [[Text Editor]] augments the standard structured editor of Rodin with a text editor.
+
Each page shall be quite short (ca. 4-5 printed pages as the D45 contains 7 sections).<br>
* [[Records_Extension|Records]] provide structured types for Event-B.
+
Each section is decomposed into 5 paragraphs. <b>For each topic, a subparagraph should be written.</b><br>
* [[UML-B]] provides a 'UML-like' graphical front end for Event-B.
 
* [[Parallel Composition using Event-B]] allows the composition of machines through events for Event-B.
 
* [[Decomposition Plug-in User Guide|Decomposition Plug-in]] allows the decomposition of Event-B machines/contexts (shared variables (A-style) and shared events decomposition (B-style))
 
* [[Refactoring Framework]] allows the refactoring of elements that are part of file (and also on related files).
 
* [[Rose (Structured) Editor]] a model structured editor.
 
* [[Flows]] plug-in allows the addition of control flow to a machine.
 
* [[Image:Mlogo_big.png|40px]] [[Modularisation Plug-in]] provides a mechanism for constructing and proving modular developments.
 
* [[Mode/FT Views]] plug-in brings modelling of modal and fault tolerance features.
 
* [[Team-based development]] enables Event-B models to be stored in a shared repository (e.g. SVN).
 
  
=== Animation ===
+
=== Overview ===
* [[ProB]] is an animator and model checker for the B-Method,
+
This first paragraph shall identify the involved partners and give an overview of the contribution. In particular, it shall provide answers to the following questions:
* [[Image:AnimB.png|50px]] [[AnimB]] is an animator for the Rodin platform,
+
* What are the common denominations?
* [[UML-B - Statemachine Animation]] provides an animation (using Pro-B) of UML-B State-machines,
+
* Is it a new feature or an improvement?
 +
* What is the main purpose?
 +
* Who was in charge?
 +
* Who was involved?
  
=== Documentation ===
+
=== Motivations ===
* [[ReqsManagement]] offer supports for requirements management.
+
This paragraph shall express the motivation for each tool extension and improvement. More precisely, it shall first indicate the state before the work, the encountered difficulties, and shall highlight the requirements (eg. those of industrial partners). Then, it shall summarize how these requirements are addressed and what are the main benefits.
* [[B2Latex]] allows to typeset an event-B model with latex,
 
  
=== Theory and Proof ===
+
=== Choices / Decisions ===
* [[Theory Plug-in|Theory Plug-in]] provides capabilities to extend the Event-B mathematical language and the Rodin proving infrastructure.
+
This paragraph shall summarize the decisions (eg. design decisions) and justify them. Thus, it may present the studied solutions, through their main advantages and inconvenients, to legitimate the final choices.
* [[Proof Purger Interface|Proof Purger]] offers to delete unused proofs.
 
* [[Proof Skeleton View]] displays the skeleton of existing proofs.
 
* [[SMT Plug-in]] provides interface for SMT solvers.  
 
* [[Relevance Filter Plug-in]] Uses heuristics to filter hypotheses shown to the prover
 
  
=== Code Generation ===
+
=== Available Documentation ===
* [[Code Generation|Multitasking code generation]] supports generation of multi-tasking Ada code from Event-B.
+
This paragraph shall give pointers to the available wiki pages or related publications. This documentation may contain:
* [[B2C plugin|B2C]] translates Event-B models to C source code, which may then be compiled using external C development tools.
+
* Requirements.  
 +
* Pre-studies (states of the art, proposals, discussions).
 +
* Technical details (specifications).
 +
* Teaching materials (tutorials).
 +
* User's guides.
 +
A distinction shall be made on the one hand between these different categories, and on the other hand between documentation written for developers and documentation written for end-users.
  
=== Experimental ===
+
=== Status ===
* [[Group refinement plugin|Group Refinement]] changes the set of refinement laws for one refinement step to facilitate a case of atomicity refinement.
+
This paragraph shall give the current status of the work being done for a given topic (as of 27 Apr 2012).
* [[Model Critic]] is an extension using the Epsilon scripting language to analyse Event-B models
 
* [[Feature Composition Plug-in]] allows the composition of Event-B features (machines|contexts) and helps the user in resolving conflicts before composition.
 
* [[Feature Modelling Tool]] (prototype) can be used to build feature models for product lines and configure these to generate product line members.
 
* [[Pattern]] allows the reusing of existing models within a development in order to save the modelling and proving effort.
 
* [[Image:Project diagram icon s.png]] [[Project Diagram]] displays the diagram of a Rodin project.
 
* [[Export to Isabelle]] exports proof obligations to Isabelle/HOL
 
* [[Image:IUMLB.png]] [[Event-B Statemachines]] adds state machines directly to your Event-B models and also allows to animate them.
 
  
== Rodin Plug-in Tutorials ==
+
== Formatting rules ==
* [[UML-B Tutorial]]
+
In order to homogeneize the contributions and to ensure consistent spelling the following formatting rules shall be enforced:
* [[Requirements Tutorial]],
+
* See §4 of [http://wiki.event-b.org/images/Llncsdoc.pdf How to Edit Your Input File] for LLNCS formatting rules.
* [[AnimB Flash Tutorial|Flash Animation Tutorial]] with animB and Adobe CS3.
+
* DEPLOY and Rodin shall be typed this way.
* [http://deploy-eprints.ecs.soton.ac.uk/227/ Modularisation Tutorial]
+
* Contractions shall not be used (eg. write "does not" instead of "doesn't", "let us" instead of "let's", etc).
== Tips & Tricks ==
+
* British english spelling shall be retained.
 +
* "plug-in" shall be preferred to "plugin".
 +
* Remember that the document is dated 27 Apr 2012, use past, present and future accordingly.
 +
* The dedicated category, <nowiki>[[Category:D45 Deliverable]]</nowiki>, shall be specified for wiki pages.
 +
* If you intend to use the same reference multiple times, please use the Cite extension [http://www.mediawiki.org/wiki/Extension:Cite/Cite.php] that has been installed since the D32.
 +
: By doing so, you will have to add the additional paragraph (below) at the end of the page you complete:
 +
==References==
 +
<nowiki><references/></nowiki>
 +
: Note that you can add references using the normal wikimedia links as well as using references nevertheless only the latter ones will appear in the references section on the wiki (e.g. all references will appear in the final PDF document whatever their type).
  
* [[Installing external plug-ins manually]]
+
== Deploy Deliverable ==
 +
=== D45 ===
  
[[Category:User documentation]]
+
 
[[Category:Plugin]]
+
:[[D45 Introduction|Introduction]] (Laurent Voisin)
 +
:[[D45 General Platform Maintenance|General Platform Maintenance]]
 +
:*Platform maintenance (Thomas Muller)
 +
 
 +
:*Mathematical extensions / Theory Plug-in (Issam Maamria)
 +
 
 +
:*Plug-in Incompatibilities (All partners)
 +
 
 +
:*Modularisation (Alexei Illiasov)
 +
 
 +
:*Decomposition (Renato Silva)
 +
 
 +
:*Team-based Development (Colin Snook, Vitaly Savicks)
 +
 
 +
:*UML-B (Colin Snook, Vitaly Savicks)
 +
 
 +
:*ProR (Michael Jastram)
 +
 
 +
:[[D45 Scalability|Scalability]]
 +
:*Improved performance (Laurent Voisin, Nicolas Beauger, Thomas  Muller)
 +
 
 +
:*Design Pattern Management / Generic Instantiation (Thai Son Hoang)
 +
 
 +
:*Edition (Thomas Muller, Ingo Weigelt)
 +
 
 +
:[[D45 Prover Enhancement|Prover Enhancement]]
 +
 
 +
:*New rewriting and inference rules (Laurent Voisin)
 +
 
 +
:*Advanced Preferences for Auto-tactics (Nicolas Beauger)
 +
 
 +
:*Isabelle Plug-in (Matthias Schmaltz)
 +
 
 +
:*ProB Disprover (Daniel Plagge, Jens Bendiposto)
 +
 
 +
:*SMT Solver Integration (Laurent Voisin)
 +
 
 +
:[[D45 Code Generation|Code Generation]] (Andy Edmunds)
 +
 
 +
:[[D45 Model-based testing| Model-based testing]] (Michael Leuschel, Alin Stefanescu)
 +
 
 +
:[[D45 Model Checking|Model Checking]] (Michael Leuschel)
 +
 
 +
[[Category:D45 Deliverable]]
 +
[[Category:Books]]

Revision as of 11:37, 7 November 2011

Template:Saved book

Introduction

The purpose of this page is to give a base for the final DEPLOY Deliverable D45 (Model Construction tools & Analysis IV) which will be delivered to the European Commission (27 April 2012).

Template

For each section covered in this document, a wiki page has been created and shall be completed (see Contents). Each of them should give a brief description of the work that was carried on during the last year of the project (Feb 2011-April 2012 [Extension included]) within the WP9 package, without going deeply into technical details.

Goal: give to the project reviewers some insight which should look like an executive summary on a given WP9 topic.
All details (papers, detailed wiki pages, etc.) should be made available as pointers.

This template provides a common structure for all of these pages.
Each page shall be quite short (ca. 4-5 printed pages as the D45 contains 7 sections).
Each section is decomposed into 5 paragraphs. For each topic, a subparagraph should be written.

Overview

This first paragraph shall identify the involved partners and give an overview of the contribution. In particular, it shall provide answers to the following questions:

  • What are the common denominations?
  • Is it a new feature or an improvement?
  • What is the main purpose?
  • Who was in charge?
  • Who was involved?

Motivations

This paragraph shall express the motivation for each tool extension and improvement. More precisely, it shall first indicate the state before the work, the encountered difficulties, and shall highlight the requirements (eg. those of industrial partners). Then, it shall summarize how these requirements are addressed and what are the main benefits.

Choices / Decisions

This paragraph shall summarize the decisions (eg. design decisions) and justify them. Thus, it may present the studied solutions, through their main advantages and inconvenients, to legitimate the final choices.

Available Documentation

This paragraph shall give pointers to the available wiki pages or related publications. This documentation may contain:

  • Requirements.
  • Pre-studies (states of the art, proposals, discussions).
  • Technical details (specifications).
  • Teaching materials (tutorials).
  • User's guides.

A distinction shall be made on the one hand between these different categories, and on the other hand between documentation written for developers and documentation written for end-users.

Status

This paragraph shall give the current status of the work being done for a given topic (as of 27 Apr 2012).

Formatting rules

In order to homogeneize the contributions and to ensure consistent spelling the following formatting rules shall be enforced:

  • See §4 of How to Edit Your Input File for LLNCS formatting rules.
  • DEPLOY and Rodin shall be typed this way.
  • Contractions shall not be used (eg. write "does not" instead of "doesn't", "let us" instead of "let's", etc).
  • British english spelling shall be retained.
  • "plug-in" shall be preferred to "plugin".
  • Remember that the document is dated 27 Apr 2012, use past, present and future accordingly.
  • The dedicated category, [[Category:D45 Deliverable]], shall be specified for wiki pages.
  • If you intend to use the same reference multiple times, please use the Cite extension [1] that has been installed since the D32.
By doing so, you will have to add the additional paragraph (below) at the end of the page you complete:
==References==
<references/>
Note that you can add references using the normal wikimedia links as well as using references nevertheless only the latter ones will appear in the references section on the wiki (e.g. all references will appear in the final PDF document whatever their type).

Deploy Deliverable

D45

Introduction (Laurent Voisin)
General Platform Maintenance
  • Platform maintenance (Thomas Muller)
  • Mathematical extensions / Theory Plug-in (Issam Maamria)
  • Plug-in Incompatibilities (All partners)
  • Modularisation (Alexei Illiasov)
  • Decomposition (Renato Silva)
  • Team-based Development (Colin Snook, Vitaly Savicks)
  • UML-B (Colin Snook, Vitaly Savicks)
  • ProR (Michael Jastram)
Scalability
  • Improved performance (Laurent Voisin, Nicolas Beauger, Thomas Muller)
  • Design Pattern Management / Generic Instantiation (Thai Son Hoang)
  • Edition (Thomas Muller, Ingo Weigelt)
Prover Enhancement
  • New rewriting and inference rules (Laurent Voisin)
  • Advanced Preferences for Auto-tactics (Nicolas Beauger)
  • Isabelle Plug-in (Matthias Schmaltz)
  • ProB Disprover (Daniel Plagge, Jens Bendiposto)
  • SMT Solver Integration (Laurent Voisin)
Code Generation (Andy Edmunds)
Model-based testing (Michael Leuschel, Alin Stefanescu)
Model Checking (Michael Leuschel)