From Event-B
Revision as of 12:00, 26 March 2010 by Jrloria (talk | contribs)
Jump to: navigation, search


Requirements Management is a crucial aspect of system development. Even a proven B-Model is useless if it doesn't realize the desired requirements. The objective of the requirements plug-in is to allow traceability between requirements and Event-B Models.

The Requirements Plugin...

  • Manages Text-Based Requirements
  • Requirements are managed and edited in an external Tool (currently Latex, Plain Text or OpenOffice)
  • Multiple Requirement Specifications can be managed in a Requirements Project.
  • A Requirements Project manages Links between individual requirements and the Event-B Specification.

User Documentation

You find the User Documentation in the form of a Requirements Tutorial.

Developer Documentation

The Requirements Plug-in has the plug-in ID fr.systerel.reqsmgr


Error creating thumbnail: Unable to save thumbnail to destination

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.

Package Structure

The package name space is fr.systerel.reqsmgr

  • The elements package contains the interfaces to the entities inside Rodin, which are Associations, Documents and Requirements. The elements.basis package provides implementations of these interfaces. This package is a good starting point for understanding the data structures.
  • The external_docs package contains the interfaces to entities outside Rodin, which are Document, ExternalRequirement, etc.