Requirements Tutorial

Introduction

This tutorial walks the user through using the Systerel Requirements Plug-In for Rodin. This Plug-In allows:

• Requirements to be edited in a set of documents (independently from Rodin)
• Requirements to be viewed within Rodin
• Individual Requirements to be linked to individual Event-B-Entities
• A basic completion test to be performed

This Plug-In is not yet officially part of Rodin and therefore not supported yet. Version 1 of the Plug-In is planned for September 2008.

Glossary

Parser

Each Requirements Document must be associated with a Parser that can extract requirements from the document. The Parser may require configuration.

Requirement

In this context, a Requirement is "a documented condition or property" of the system.

Requirements Document

A container for Requirements and optionally additional information (e.g. Headlines, explanatory texts, etc.)

Requirements Map

A .req-File within a Rodin Project that associates Requirements Documents with Event-B Specifications

Installation

As the Plug-In is currently under development, it has to be installed manually. Alternatively, it can be built and deployed together with the Rodin sources. This exercise is left for advanced users.

To deploy the Requirements Plug-In:

• Install the Plug-In from the Düsseldorf Update site at http://www.stups.uni-duesseldorf.de/update
• Unzip the file and copy the contents into your Rodin Plug-In directory

That's it! After restarting Rodin, you can check whether the Plug-In got installed successfully by opening Help > About Rodin Platform and clicking on Plug-In Details. The Plug-In should be listed as shown in the following screenshot:

Architecture

In order to manage Requirements in Rodin, a Requirements Map must be created. This Map is part of a Project. It keeps track of Requirements Documents that are managed outside of Rodin. Currently, Plain Text, Latex and OpenOffice are supported.

Each Requirements Document is broken into Requirements. Within Rodin, only textual Requirements are visible and Formatting is lost. Individual Requirements can then be marked as relevant and fulfilled, and can be linked with individual Event-B-Elements.

All additional information (links, fulfillment information, etc.) is stored in the Map, nothing is stored in the Requirements Documents or Event-B.

More than one Map can be created. This could be useful for different relationships, e.g. "fulfills", "tests", etc.

Enabling the Navigator View

Requirements Documents are not shown in the Project Explorer. In order to work with the Requirements Plug-In, you need to work with the Navigator View. You can open it via Window > Show View > Other... The Navigator View can be found under General > Navigator.

The addition of the view only affects the current Perspective.

Creating a Requirements Map

Currently, the Requirements Map must be created manually:

• Create a file with the extension .req within a Rodin Project
• Seed the file with the following content:

<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<root>
</root>

• You can now open the file from the Navigator view. To do so, either doubleclick the file or select Open With > Requirements Editor from the context menu.

Adding a Requirements Document

You need a specification before you can add one to the Requirements Map. Three formats are currently supported, but as of 22-July-2008, only the connectors for Plain Text and LaTex are working. The formats are described further down, here is a Sample Plain Text Requirements Specification that we are going to use to demonstrate the Plug-In's features.

The Requirements Editor has an "Add document" button on the "Requirements documents" tab. Add a document by clicking this button and selecting the Requirements Document from the file system. The Requirements Editor should now look as follows:

We set a parser by right-clicking the highlighted row and selecting "Set Parser" from the context menu. We pick the appropriate parser, in this case "Plain Text Requirements Parser".

Note: The context menu contains entries that are not meaningful in this context and should be ignored (they will be removed someday).

Synchronizing Requirements

The reading of the requirements for the requirement document(s) must be triggered explicitly. To do so, we press the "Synchronize" Button. The results of the synchronization will be shown in a dialog.

To see whether our synchronization was successful, we switch to the "Requirements" tab. It should look like this:

Note 1: While Identifier and Document can be edited here, it shouldn't be done (changes will be lost upon next synchronization).

Note 2: Another View "Requirement details" exists that shows the content of "Text" of the selected requirement.

The "relevant" flag can be unset for requirements that are not relevant to the Event-B machine (e.g. non-functional requirements). Likewise, requirements can be marked manually as "fulfilled".

Linking Requirements

Links are created from the Project Explorer. Most elements of Contexts and Machines can be linked. You can see that an element can be linked from its context menu. To link an element:

• Select exactly one requirement in the Requirement Editor
• Right-click on the Event-B-Element to be linked in the Project Explorer
• Select Requirements Manager > Add Association
• The link will be shown in the requirements view underneath the associated requirement
• The link will also be shown in the Project Explorer underneath the linked element
• n:m-relationships are possible
• From the Project Explorer, you can navigate to a linked requirement through the context menu.

Parser Settings

The plain text parser is a minimal parser that doesn't require configuration. However, all parsers can be configured further. The configuration dialog can be access from the "Requiremnts documents" tab by right-clicking on an entry and selecting "Edit Parser Settings" from the context menu.

Every parser has different parameters. The values for the parameters can be set in the "Value" column.

Check Model Completeness

TODO

Parsers

OpenOffice Parser

tbd