Rodin tool

The Rodin tool, is a tool for formal modelling in Event-B. Event-B is a notation and method developed from the B-Method and is intended to be used with an incremental style of modelling. The idea of incremental modelling has been taken from programming: modern programming languages come with integrated development environment that make it easy to modify and improve programs. The Rodin tool provides such an environment for Event-B. The two main characteristics of the Rodin tool are its ease of use and its extensibility. The tool focuses on modelling. It is easy to modify models and try out variations of a model. The tool can also be extended easily. This makes it possible to adapt the tool to specific needs, so the tool can be adapted to fit into existing development processes instead of demanding the opposite. The Event-B wiki is a useful user and developer resource.

Rodin (Rigorous Open Development Environment for Complex Systems) is and extension of Eclipse IDE (Java based). Rodin Eclipse Builder coordinates:

Rodin Proof Manager (PM)

Industrial applications and case studies

The Rodin project included five industrial case studies that served to validate the tool set and helped with the elaboration of an appropriate methodology for using the tools. The case studies were led by industrial partners of the Rodin project supported by the other partners. The case studies were as follows:

Some available plug-ins for Rodin

References

This article is based on material taken from the Free On-line Dictionary of Computing prior to 1 November 2008 and incorporated under the "relicensing" terms of the GFDL, version 1.3 or later.

This article is issued from Wikipedia - version of the Friday, February 12, 2016. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.