Problems in using Rodin Platform in Deploy WP3

This is an informal report authored by Kimmo Varpaaniemi on 2008-10-18. Though this report is a contribution of SSF (Space Systems Finland Ltd.) to Deploy WP3, nothing in this report should be considered as an official statement of SSF.

Introduction

As described in http://bscw.cs.ncl.ac.uk/bscw/bscw.cgi/d91253/BepiColombo%20-%20Modelling%20Approach.pdf, SSF uses Rodin Platform for modelling of BepiColombo SIXS (Solar Intensity X-ray Spectrometer) / MIXS (Mercury Imaging X-ray Spectrometer) OBSW (On-Board SoftWare) requirements. The Event-B project BepiColombo_Models_v3.3 in the archive http://bscw.cs.ncl.ac.uk/bscw/bscw.cgi/d92074/BepiColombo_Models_v3.3.zip is a coarse model for that purpose. Creating that project and producing the proofs in that project were still efforts big enough for serious usability problems to be observed in Rodin Platform. Note that problems primarily due to the Event-B language are not considered in this report. (For example, cumulative data replication in refinement chains and lack of modularity are primarily due to the Event-B language.)

Auto-proving

The BepiColombo_Models_v3.3 project is simple enough for a computer scientist to write a program that deduces all the theorems, axioms and well-definedness criteria from the axioms, event guards and event actions. It therefore took some time to get over the disappointment that Rodin Platform is not able to prove all those properties automatically and that in some cases it is more comfortable to produce a proof interactively than to find out whether Rodin Platform is able to produce a proof automatically.

Checking of auto-provability too often induces a reported internal error or makes Rodin Platform non-responding. Such situations tend to be associated with memory consumption that very observably slows down other activities in the computer where the Rodin Platform process is run. Paradoxally, memory consumption and its side effects do not properly justify a bug report against Rodin Platform as long as there is no evidence that Rodin Platform would have "exceeded its memory budget". Memory consumption without "safe limits" is a widely accepted practice in e.g. model checking tools.

The file http://bscw.cs.ncl.ac.uk/bscw/bscw.cgi/d92271/AutoStatus.pdf displays a history of a Rodin Platform 0.8.2 session in a Windows XP environment by means of screen captures. As displayed by the first and the second screen capture, the initial configuration of tactics is such that every available tactic is allowed to be used. From the third and the fourth screen capture we see that after being imported, the BepiColombo_Models_v3.3 project is the only Event-B project in the used workspace. As suggested by the fourth, fifth and sixth screen capture, the only post-import activity by the user is to, on the context level, ask Rodin Platform to re-check auto-provability of all theorems in the three contexts sixsp_C0, mixst_C0 and mixsc_C0, in that order. The seventh screen capture displays the last theorem that occurs in the progress information window before Rodin Platform acknowledges a Java heap space problem. That acknowledgement is displayed by the eighth (also the last) screen capture.

The file http://bscw.cs.ncl.ac.uk/bscw/bscw.cgi/d92284/AutoStatus2.pdf displays a history of a Rodin Platform 0.8.2 session in another Windows XP environment by means of screen captures. The initial configuration, the imported project and the user activities on Rodin Platform are the same as in the above-described session, except that the user has no chance to proceed beyond sixsp_C0 because Rodin Platform becomes non-responding. An attempt to produce a screen capture for the last observed non-blank contents of the progress information window failed because Rodin Platform's non-response was associated with memory consumption that strongly delayed screen capturing and made it difficult to produce screen captures for contents not reproducible by refreshing the screen. The last observed non-blank contents of the progress information window referred to the theorem thm7 of sixsp_C0.

The configuration of tactics in the above examples is not inherently impractical: using that configuration, recalculation of auto statuses of the machines csw_M0, mixsc_M0, mixst_M0, sixsp_M0 and sixsx_M0 in the BepiColombo_Models_v3.3 project takes very few minutes only and increases the number of automatically proven invariants in each one of those machines. It is still true that phenomena demonstrated in the above examples can to some extent be avoided e.g. by using Rodin Platform's default configuration that does not allow use of every available tactic. The documentation of Rodin Platform 0.8.2 has no "survival guide" for users who with reasonable risks are ready to experiment with "advanced" configurations of tactics.

Rodin Platform 0.8.2 has a "Build Automatically" option that is on by default and can be set on or off in the "Project" menu. Whenever a context or a machine is saved and that option is on, every potentially affected context and machine of the containing project is re-checked. So, if the configuration of tactics is as in the above examples, mere saving a context or a machine may end up in a situation similar to the end situations in those examples. (It is somehow frustrating that any new theorem has to be considered as a potential key hypothesis for automated proofs of properties that have already been proven interactively.) The documentation of Rodin Platform 0.8.2 does not mention the "Build Automatically" option.

Interactive proving

In many of the interactive proofs in the BepiColombo_Models_v3.3, user activities are limited to: choosing the default prover, pruning the original proof tree, and choosing the used hypotheses. In choosing the used hypotheses, it suffices for the user to mechanically apply some criteria so simple that it is difficult to understand why such criteria are not built in the tool.

When the above-mentioned user activities do not suffice for obtaining a proof, a user easily ends up in clicking whatever can be clicked, without necessarily much idea of what is defined to happen as a result of the clicking. As such half-random clicking actually often produces a proof, the tool could apparently do the same thing on behalf of the user.

To put it bluntly: facilities for interactive proving are best improved by eliminating the need for using them. Pragmatic documentation for interactive proving in Rodin Platform is perhaps the next best thing to do. (It is questionable to arrange training days just to compensate missing documentation.)

Editing in contexts and machines

Considering contexts and machines, let us the term "logical line" to mean a definition that starts with a label and is not the definition of a whole event. Though the order of logical lines has an important role in the semantics of Event-B projects, the editor for contexts and machines in Rodin Platform 0.8.2 seems to do its best to discourage moving of logical lines. Possibly the easiest provided way to move a logical line is to press a mouse button as many times as the new position differs from the old position. Except for the special case formed by a single event, possibly the easiest provided way to move a block of logical lines is to move the logical lines in the block one by one.

The provided default labels work as effective local line numbers, so a user may want to preserve the order of local line numbers regardless of the contents of the lines. Possibly the easiest provided way to ensure "increasing local line numbering" is to edit the numeric suffixes in the labels. (There have been situations where the tool's internal mapping between labels and labelled entities has been suspected to be different from what is displayed. Such situations have occurred when labels have been edited.)

Exporting a project

When an Event-B project is exported by Rodin Platform 0.8.2, the contents of the produced archive is determined by what is known by the resource navigator. Unfortunately, the resource navigator does not even try to be in synchrony with the actual file system. (Such a lack of synchrony is likely intentional because the phenomenon is striking enough to have been observed long ago.) After a few export/import surprises, a user slowly learns to refresh the knowledge of the resource navigator before exporting a project.