Difference between revisions of "Requirements Tutorial"

From Event-B
Jump to navigationJump to search
imported>Mathieu
imported>Jastram
 
(7 intermediate revisions by 2 users not shown)
Line 1: Line 1:
 +
{{TOCright}}
 
= Introduction =
 
= Introduction =
  
Line 7: Line 8:
 
* Individual Requirements to be linked to individual Event-B-Entities
 
* Individual Requirements to be linked to individual Event-B-Entities
 
* A basic completion test to be performed
 
* 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 =
 
= Glossary =
Line 19: Line 18:
 
= Installation =
 
= 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.
+
As of Rodin 0.9.0, the Requirements Plug-In can be installed via the Eclipse update mechanismTo do so, follow the following steps:
 
 
To deploy the Requirements Plug-In:
 
 
 
* [[Media:fr.systerel.reqsmgr-2008-07-22.zip|Download]] the Plug-In
 
* 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 DetailsThe Plug-In should be listed as shown in the following screenshot:
 
 
 
[[Image:About-Dialog.png]]
 
  
= Architecture =
+
* Start Rodin
  
[[Image:rodin-requirements.png|right]]
+
* Select from the menu: Help > Software Updates > Find and Install...
  
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.
+
* On the dialog, select "Search for new features to install" and press Next
  
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.
+
* On the next page, select "ProB update site" and click Finish
  
All additional information (links, fulfillment information, etc.) is stored in the Map, nothing is stored in the Requirements Documents or Event-B.
+
* 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)
  
More than one Map can be created.  This could be useful for different relationships, e.g. "fulfills", "tests", etc.
+
* That's it!  Now you can now start using the Plug-In
  
 
= Enabling the Navigator View =
 
= Enabling the Navigator View =
Line 50: Line 40:
 
= 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.
 +
 
 +
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.
  
* Create a file with the extension .req within a Rodin Project
+
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).
* Seed the file with the following content:
+
 
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+
Upon creation, the Requirements Map Editor is opened.
<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 =
 
= 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 workingThe 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.
+
You need a specification before you can add one to the Requirements Map.  Three formats are currently supported (see below)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:
 
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:
Line 103: Line 92:
 
Every parser has different parameters.  The values for the parameters can be set in the "Value" column.
 
Every parser has different parameters.  The values for the parameters can be set in the "Value" column.
  
= Check Model Completeness =
+
= Parsers =
  
{{TODO|}}
+
The Requirements Plug-In provides an open architecture that makes it easy to implement parsers for various data types.  The following parsers are currently available:
  
= Parsers =
+
== Plain Text Parser ==
 +
 
 +
A very simple implementation that is useful for demonstrations.  This Parser cannot be configured in any way, and it expect the following format:
 +
 
 +
* Each requirement starts with the label "Requirement:"
 +
* The label is followed by the Requirement-identifier, consisting of a text part, followed by a hyphen, followed by a number (e.g. FUN-1)
 +
* The requirements text starts on the next line and may span multiple lines
 +
* Repeat for every requirement.
 +
 
 +
Example:
  
== Plain Text Parser ==
+
Requirement: FUN-17
 +
 +
Text describing the requirement
  
 
== LaTeX Parser ==
 
== LaTeX Parser ==
  
== OpenOffice Parser ==
+
A parser that can be configured to detect various Latex-Constructs, using regular expressions.
 +
 
 +
* This parser must be configured (right-click on the entry of the requirements map and select "Edit parser settings")
 +
* The individual settings are documented in the interface
 +
 
 +
There are a few pitfalls: First, the regular expressions are greedy and don't stop at line breaks.  Second, the regular expressions use the Java-Syntax which differs from the grep syntax.  It is documented [http://java.sun.com/j2se/1.4.2/docs/api/java/util/regex/Pattern.html here].
 +
 
  
tbd
 
  
 +
== OpenOffice Parser ==
 +
A parser that processes OpenOffice documents.
  
[[Category:User Documentation]]
+
[[Category:User documentation]]
 
[[Category:Requirement Plugin]]
 
[[Category:Requirement Plugin]]
 
[[Category:Tutorial|Requirement Plugin]]
 
[[Category:Tutorial|Requirement Plugin]]

Latest revision as of 15:44, 25 February 2009

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

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

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 (see below). 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.

Parsers

The Requirements Plug-In provides an open architecture that makes it easy to implement parsers for various data types. The following parsers are currently available:

Plain Text Parser

A very simple implementation that is useful for demonstrations. This Parser cannot be configured in any way, and it expect the following format:

  • Each requirement starts with the label "Requirement:"
  • The label is followed by the Requirement-identifier, consisting of a text part, followed by a hyphen, followed by a number (e.g. FUN-1)
  • The requirements text starts on the next line and may span multiple lines
  • Repeat for every requirement.

Example:

Requirement: FUN-17

Text describing the requirement

LaTeX Parser

A parser that can be configured to detect various Latex-Constructs, using regular expressions.

  • This parser must be configured (right-click on the entry of the requirements map and select "Edit parser settings")
  • The individual settings are documented in the interface

There are a few pitfalls: First, the regular expressions are greedy and don't stop at line breaks. Second, the regular expressions use the Java-Syntax which differs from the grep syntax. It is documented here.


OpenOffice Parser

A parser that processes OpenOffice documents.