ProR

ProR is a tool for editing requirements, part of the Eclipse Requirements Modeling Framework (RMF). An integration with Rodin exists.

General Usage

ProR supports creating a hierarchical requirements structure. Requirements are presented in a table-view. Creating annotated links between requirements is supported. To find out more about the general functionality, please visit the RMF page at eclipse.org. In particular, the short video there provides a quick overview on the usage of ProR.

Rodin Integration

An integration plugin has been created for Rodin. The following is a very quick'n'dirty tutorial on how to use it.

Specification / Use Cases

Feel free to consult the Specification of the integration plugin: File:Pror-integration.pdf

How to install?

The ProR Rodin Integration is installed via an update site. Starting with Rodin 2.5, the update site for the integration plugin is already included. Otherwise, here are the current available update sites:

Update Site: http://update.formalmind.com/rodin

Tutorial

Starting a new Integration Project

To start a new integration project, create a new ReqIF Model for Event-B integration via:

File > New > Other... > ProR (Reqif) > ReqIF Event-B Model

This should bring up the New ReqIF file wizard where you have to enter the relevant data needed for creating a new ReqIF file.

• Select an Event-B Project where you want to create a new ReqIF file (for instance the project "Lift").
• Enter a valid, i.e. non empty and non-existing name for the new ReqIF file, for instance "Specification.reqif".
• With a click on the "Finish" button the new ReqIF file will be created and displayed in the Lift Event-B project folder.
• The ReqIF editor opens automatically.

Please note: This Model is already preconfigured with all required presentations. If you start from an existing ReqIF model, you need to configure those presentations manually. Please check out the spec above to find out about them.

Creating Links from Event-B to ProR

Manual creation of traces between requirements and formal model elements is supported via drag and drop. Simply drag Event-B elements from the Event-B Explorer (you can unfold models there) right into the Specification Editor. This will create a trace. In order to see the created traces, you have to click on the small "triangle" icon in the tool bar menu.

The right column “Link” of the specification editor summarizes the number of outgoing (target) and incoming (source) traces. Selecting an outgoing trace shows the targets properties in the Properties View. In addition, traces can be annotated if additional information is necessary.

Inserting Model Elements into the Requirements Model

This is right now a little awkward:

• Create a trace as described above
• Create a new SpecHierarchy in the Specification Editor
• In the properties view, set the "Object" property to the Rodin Element that you would like to show.

We're working on enabling this through drag and drop as well.

Color Highlighting

All identifiers from the Event-B model should be recognized in the Description field of the Specification Editor. In order to mark an identifier the corresponding text passage is put in square brackets.

• Red marked text passages reminds the user that an undeclared identifier is used.
• Blue marked text passages are recognized phenomena.
• Unmarked, recognized identifier are highlighted as well (underlined in red) the text passage to warn the user about a possible omission.

All colors are explained by a tool tip as well. The tool tip appears just when you roll on with the mouse (hover).

Tracking Changes

When traced formal model elements change, the trace is marked as “suspect” by showing a small icon. Two columns exist for the source and the target of the trace, respectively. The user sees at a glance which requirements or formal model elements need to be revalidated. This is particularly useful if the requirements document becomes large. By double-clicking on the “suspect” icon, the user can mark the trace as “revalidated’’ and the icon will be removed.

Known Problems

• Pasting (and copying) in the cell with the highlighting is currently not possible. A workaround is to temporarily disable the corresponding plug-in. Then copy and paste works, but only through the context menu.
• ReqIF Files are currently not shown in the Rodin Explorer. To see (and open), please use the Navigator View instead.
• Terminating editing with a carriage return inserts a linebreak. Better finish editing by clicking outside the cell.
• Renaming the Event-B project will destroy the created links. You have to open the ReqIF file with a text editor and replace the old Event-B project name with the new one at the corresponding places.

Roadmap

• There are still some limitations on the ProR/Rodin integration plugin, however. While all required data structures exist, the plugin would benefit from more sophisticated reporting. In particular, lists a number of properties of a correct system description. While the presence of these properties does not guarantee correctness, their absence indicates a problem. Reporting on the state of these properties would be valuable.

• Furthermore, the plugin does not support classifying phenomena. In a next step we will work on a concept for classifying and maintaining phenomena with ProR.

• Jump to Rodin Editor via context menu