Requirements Tutorial

From Event-B
Revision as of 14:05, 22 July 2008 by imported>Jastram (New page: = 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 (independ...)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to navigationJump to search

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

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:

  • 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 Details. The Plug-In should be listed as shown in the following screenshot:

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 Document