Documentation Overhaul DoW

From Event-B
Jump to: navigation, search


This project is currently in the second iteration, which is scheduled to end on October 8th 2011. The continuous build of the handbook can be found at

NOTE: "mh" means man-hours

Representatives of Stakeholders

We need volunteers willing to represent the stakeholders. So far we have:

  • Cliff Jones - representing the contracting body (Deploy)
  • Rainer Gmehlich - representing an industrial partner (Bosch)
  • Andreas Roth - representing an industrial partner (SAP)
  • Aryldo G Russo Jr - representing an associate (AES)
  • Carine Pascal - representing Systerel
  • Lukas Ladenberger - representing an academic partner (UDUS)
  • Matthias Schmalz - representing an academic partner (ETHZ)

The task of the reviewers is to provide feedback in a timely manner.

First Iteration

WP1-1: Styles Guides and Templates (16mh)

Once we decide on the form for the documentation, we will create a style guide to ensure consistency. We will also provide templates as needed, to simplify the creation of the documentation.

Deliverable: A Guideline for content creators and templates to go with it.

WP1-2: Wiki Migration or Version Plan (4mh)

Content must be accessible at all times. However, we will either migrate or restructure data significantly. We need a plan describing the approach.

Deliverable: A Guideline for content migration: Handbook Content Migration

WP1-3: Reference Section (20mh)

The Reference Section will be the most comprehensive part of the documentation. It will consist of a number of chapters. At this point we see at least the following sections:

  • Event-B Reference
  • Mathematical Notation Reference
  • Modeling Language Reference
  • Proof Tactics
  • GUI Elements
  • Glossary

There may be more. We must have a good understanding of the content we intend to cover. Otherwise we won't be able to allocate our resources wisely.

The FAQ will grow naturally and won't need a detailed plan beforehand.

Deliverable: The table of contents of the reference section (1st and maybe 2nd level)

WP1-4: Tutorial outline (20mh)

The tutorial is most likely the first thing new users are being confronted with. Thus, we feel that this chapter requires a lot of diligence. Also, we will perform user tests with the tutorial, once created. The tutorial will guide the user through installation, ensure that the mathematical background exists, introduce the GUI and guide the user through a few modeling sessions.

We feel that the current tutorial overwhelms the user by focusing on too many aspects at the same time. For instance, we believe that the first model must allow all proofs to be discharged automatically.

Deliverable: The table of contents of the tutorial, including the description of the individual sections.

WP1-5: First iteration on Tutorial (80mh)

Our goal is to use the remaining time of the first iteration to make the tutorial rudimentary complete. This means that all examples are worked out and that most of the copy stands. There may be gaps, but only if the gaps don't impair the usefulness of the tutorial (e.g. the section on the mathematical notation may refer to the Abrial-Slides).

We expect that during this work, the rest of the documentation will start to fill up with placeholders (e.g. empty entries in the reference section.

Deliverable: The roughly completed Tutorial.

WP1-6: Iteration Review (20mh)

In addition to discussion the results so far, we will decide on the details of WP2-1.

Second Iteration

WP2-1: Migration and Creation of entries in the Reference Section (60mh)

We will start filling the reference section. We expect a number of sections to be quite labor-intensive, especially if it involves creating many screenshots.

Deliverable: Completed Parts of the Reference Section.

WP2-2: Copy Editing of existing content (60mh)

We managed to recruit Joy Clark, a native English speaking student, who will from this iteration on perform copy editing. In this iteration, she will make one complete run through the tutorial to improve copy and to identify gaps, which will then be filled.

Deliverable: Copy-edited content.

WP2-3: Guideline for Plugin Developers (20mh)

Even though Plugins are officially not covered by the handbook, there are many places where covering some aspects would be extremely useful. We will produce a guideline for Plugin developers for including references to their work in the handbook.

Deliverable: The Guideline.

WP2-4: Iteration Review (20mh)

The results will be evaluated, particularly on whether the tutorial needs more focus or not.

Third Iteration

WP3-1: Completion of the Reference Section (30h)

The goal is to fill in all blanks in the reference section at this point. We may keep a list of entries that need improvements.

Deliverable: Complete Reference Section.

WP3-2: User Tests of Tutorial (40mh)

We will offer a B block course in fall 2011 in Düsseldorf, where the students will learn classical B (not Event-B). They will get a class project in Event-B. They will have to teach themselves Event-B using the tutorial, in order to solve their assignment. We will monitor the progress, collect feedback and identify overall weaknesses in the tutorial. We expect a group of 5-10 students.

Deliverable: Results of the user tests

WP3-3: Completion of the Tutorial (20mh)

We will incorporate the feedback from the review.

Deliverable: Complete Tutorial.

WP3-4: Provide context to give the documentation a whole appearance (20mh)

At this point, we will pay attention to the document “as a whole”. We will make sure all sections have proper introductions, check the style, etc. We will also create a list of sections that need particular attention.

Deliverable: Improved documentation

WP3-5: Remove migrated content from Wiki (20h)

Eventually, we want to remove migrated content from the Wiki to prevent outdated information. At the same time, we will create a tighter integration between handbook web site and the Rodin Wiki. We'll also visit every single wiki page and if there is ambiguity on where the content should reside, we'll track down the owner and figure it out.

Deliverable: Cleaned-up Wiki.

WP3-6: Creation of an index (10mh)

An index will be created, for two reasons: First, in the print version, this will be a useful tool in addition to cross references and the table of contents. Second, it will allow the location of topics where the search functionality is simply inadequate (e.g. mathematical symbols, words like "where").

Deliverable: Index.

WP3-7: Iteration Review (20mh)

The last iteration will be used for “polishing” In this review, we allocate the resources as needed.

Forth Iteration

WP4-1: Improve Tutorial Chapters 2.9 and 2.10 (20h)

These chapters concern the celebrity problem and location access controller, and are not as well developed as the rest of the tutorial.

Deliverable: Improved Chapters 2.9 and 2.19.

WP4-2: Completion of the Reference Section (20h)

There are still some open tasks in the reference section.

Deliverable: Complete Reference Section.

WP4-3: References and "Further Reading" Sections in Tutorial (30h)

We need a tighter integration between tutorial and reference section. We will achieve this by providing more references into the reference section, and by providing a "Further Reading" section that points to the reference section and possibly to literature.

Deliverable: New subsections in each section of the tutorial, more references.

WP4-4: Coordination with Systerel to make the Rodin Handbook part of the Distribution (20h)

Currently, the handbook has to be installed manually into Rodin. We will coordinate with Systerel to make sure that the next version of Rodin will ship with the handbook already installed. We also plan to do some minor modifications on our build infrastructure.

Deliverable: Rodin with Handbook.

WP4-5: Polishing (40h)

Some screenshots and images still have to be improved, and general improvement of the text flow. Also, we will keep collecting and processing feedback from users.

Deliverable: Complete Documentation.

WP4-6: Final Review (30mh)

In addition to reviewing the last iteration, we will record feedback on the project as a whole.