2.4.1 Excursus: The specification process

While this handbook is concerned with use of the Rodin tool, it is important to understand the specification process as well. It can be daunting and unclear especially for beginners to recognize where to start with the model, what kind of data structures and abstractions to use, and so on.

We cover a few examples in this chapter that should develop your ability to answer these questions implicitly, but there is no explicit set of instructions. For example, we will first model the traffic lights as Boolean values and later refine them into actual colors. But how did we come up with this refinement strategy? Likewise, we decided to add the push buttons at a later refinement. In retrospect this may seem useful, but it is still not clear how we arrived at this structure in the first place.

Jean-Raymond Abrial has something to say about this in his book¹. Some of the chapters are available in the Rodin Wiki.

It takes some time to learn how to read formal specifications, and not all stakeholders are willing to learn it. Further, textual requiremenets are almost always the starting point for a formal specification. It would be nice to kep a traceability to the origianl requirements.

ProR is a tool for editing requirements. An integration with Rodin exists, which allows a traceability between textual requirements and model elements to be established. This shows the Event-B model elements seamless as part of the textual requirements. The various traceability options are demonstrated in the Formal Mind Blog.

Further, the traces are tracked, and if the source or the target of a trace changes, a marker is set, so that the changes can be inspected and verified.

Being able to set traces is not enough, if there is not a theory behind it to make it useful. One such theory is based on the WRSPM reference model. How this works in practice can be seen in this paper.

Last, ProR is based on the ReqIF standard, which is supported by major industry tools for requirements management (like Rational DOORS or PTC integrity). This eases the integration of Event-B into existing development processes.
This contribution requires the ProR Requirements plugin. The content is maintained by the plugin contributors and may be out of date.