Production of the Rodin Handbook

Michael Jastram and the team at Düsseldorf have done an excelent job in putting together, extending and improving various sources of documentation on the Rodin tool.

Situation

Deploy was a four-year European FP7 program with the goal of making major advances in engineering methods for dependable systems through the deployment of formal engineering methods.  Advancing and improving the professional development environment built on the Eclipse-based Rodin environment and enabling industrial users to use the platform were central objectives.

Challenge

While Rodin was already a mature software when Deploy started in 2008, its documentation was still inadequate.  It consisted of a Wiki that contained redundant and outdated information, while several parts of the software were undocumented altogether.  Further, other content existed in the form of linked PDFs, which the Wiki’s search mechanism didn’t cover.

The Deploy project management did not manage to recruit personnel for improving the documentation: Neither the academic nor the industrial partners were willing to assign resources to this task which, while important, felt mundane and less exciting than working on new technology.

Solution

Formal Mind volunteered to take on this task.  Before writing a single sentence, they made an elaborate problem analysis (an obvious first step, being experts in requirements).  From the very beginning, the Rodin community was invited and encouraged to provide feedback.  This problem analysis resulted in a solution that consisted of a central documentation repository and build process that generated three different types of documentation: PDF, HTML and Eclipse Help.

The actual writing took place in four iterations lasting roughly eight weeks each.  Again, this allowed the Rodin community to provide feedback and Formal Mind to adjust the goals of upcoming iterations accordingly.  But to be sure, Formal Mind performed a test during the third iteration.  This test required the users to build a formal specification in Event-B with the aid of the handbook, even though they neither new Event-B, nor had used Rodin before.  The results of this test led to adjustments in the final iteration.

Results

Formal Mind delivered a handbook consisting of 178 pages in the PDF version that the stakeholder were highly satisfied with.  While some content was migrated from the Wiki (and subsequently removed to prevent redundancy), the majority was newly created.

During the project, Formal Mind collected and processed 124 items of feedback from stakeholders.  They also established a continuous build system, hosted at the University of Düsseldorf, that automatically rebuilds the handbook in its various format, as soon as new content is checked into the documentation repository.

Not only were the stakeholders highly satisfied with the result, the resulting system also allows it to be maintained by any committer with some Latex knowledge, as it is well documented and automated.