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://www.stups.uni-duesseldorf.de/pror_updates

Nightly Build: http://www.stups.uni-duesseldorf.de/pror_nightly

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... > ReqIF Event-B Model

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

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.

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.

Tracking Changes

Traces to the Model have two attributes that track whether the source or target objects have changed.

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.