Difference between revisions of "Requirements Tutorial"

From Event-B
Jump to navigationJump to search
imported>Jastram
imported>Jastram
Line 54: Line 54:
 
= Creating a Requirements Map =
 
= Creating a Requirements Map =
  
Currently, the Requirements Map must be created manually:
+
A requirements map is the link between the requirements documents (managed outside Rodin) and the Event-B-Specification.
  
* Create a file with the extension .req within a Rodin Project
+
NOTE: While multiple requirements maps can be created for a project, it is recommended to create just one.  One map can manage multiple requirements documents.
* Seed the file with the following content:
+
 
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+
To create a map, simply right-click on the project and select "New Requirements Map". Alternatively, it can be created through the "New..." dialog (located at Event-B/Requirements Map).
<root>
+
 
</root>
+
Upon creation, the Requirements Map Editor is opened.
* 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 =
 
= Adding a Requirements Document =

Revision as of 13:14, 20 November 2008

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 of Rodin 0.9.0, the Requirements Plug-In can be installed via the Eclipse update mechanism. To do so, follow the following steps:

  • Start Rodin
  • Select from the menu: Help > Software Updates > Find and Install...
  • On the dialog, select "Search for new features to install" and press Next
  • On the next page, select "ProB update site" and click Finish
  • On the next dialog, you see the ProB update site. Unfold the tree, and you should see "Requirements Management". Check it, and follow the standard install procedure (accepting license, confirming the install, restart)
  • That's it! Now you can now start using the Plug-In

Architecture

Rodin-requirements.png

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

A requirements map is the link between the requirements documents (managed outside Rodin) and the Event-B-Specification.

NOTE: While multiple requirements maps can be created for a project, it is recommended to create just one. One map can manage multiple requirements documents.

To create a map, simply right-click on the project and select "New Requirements Map". Alternatively, it can be created through the "New..." dialog (located at Event-B/Requirements Map).

Upon creation, the Requirements Map Editor is opened.

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:

Requirements-map-01.png

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:

Requirements-map-02.png

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

Plain Text Parser

LaTeX Parser

OpenOffice Parser

tbd