Rodin tool

From Wikipedia, the free encyclopedia
Jump to navigation Jump to search
Rodin
Original authorsJean-Raymond Abrial, Michael Butler, et al.
DevelopersEuropean Union Projects:
  • RODIN (2004–2007)
  • DEPLOY (2008–2012)
  • ADVANCE (2011–2014)
Initial release2007
Repository
  • {{URL|example.com|optional display text}}Lua error in Module:EditAtWikidata at line 29: attempt to index field 'wikibase' (a nil value).
Written inJava
Engine
    Lua error in Module:EditAtWikidata at line 29: attempt to index field 'wikibase' (a nil value).
    PlatformEclipse IDE
    TypeSoftware tool
    LicenseOpen source
    Websitewww.event-b.org

    The Rodin tool is a software tool for formal modelling in Event-B.[1][2] It was developed as part of several collaborative European Union projects, including initially the RODIN project (2004–2007).[3]

    Overview

    [edit | edit source]

    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. Two characteristics of the Rodin tool are its ease of use and its extensibility.[2]

    The tool focuses on modelling. It allows the user to modify models and try out variations of a model. The tool is also extensible. 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. There is an associated Event-B wiki.[4]

    Rodin ("Rigorous Open Development Environment for Complex Systems") is an extension of Eclipse IDE (Java-based). The Rodin Eclipse Builder manages the following:[5]

    Rodin Proof Manager (PM)
    • PM constructs a proof tree for each PO
    • Automatic and interactive modes
    • PM manages used hypotheses
    • PM calls reasoners to:
      • discharge goal, or
      • split goal into subgoals
    • Collection of reasoners:
      • simplifier, rule‐based, decision procedures,
    • Basic tactics language to define PM and reasoners

    Industrial applications and case studies

    [edit | edit source]

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

    • A failure management system for an engine controller;
    • Part of a platform for mobile Internet technology;
    • Engineering of communications protocols;
    • An air-traffic display system;
    • An ambient campus application.

    Some available plug-ins for Rodin

    [edit | edit source]
    • B4free provers[7]
      • Provider: ClearSy
      • Function: Theorem provers
    • UML-B[8]
      • Provider: University of Southampton
      • Function: UML-like graphical front-end for Event-B supporting class diagrams and state charts
    • ProB[9][10]
      • Provider: University of Düsseldorf
      • Function: Animation and Model-checking of Event-B models; Counterexamples for false proof goals, in particular, proof obligations
    • Brama[11]
      • Provider: ClearSy
      • Function: Animation of B models. The purpose is twofold:
        • Experimentation with a model to observe states and transitions
        • Flash animation of Event-B models
    • Modularisation[12]
      • Provider: Newcastle University
      • Function: Structuring Event-B developments into logical units of modelling, called modules; Model composition; Model reuse

    References

    [edit | edit source]
    1. ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    2. ^ a b Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    3. ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    4. ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    5. ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    6. ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    7. ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    8. ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    9. ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    10. ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    11. ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
    12. ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).

    Further reading

    [edit | edit source]
    [edit | edit source]
    Retrieved from "http://70.231.62.181/index.php?title=Rodin_tool&oldid=15739729"