From Event-B
Jump to navigationJump to search

Requirements support now via ProR

The Requirements Plugin described here is deprecated and will not be developed further. Instead, the ProR platform is actively being developed.

ProR is documented at


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



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.