View source for Software:Rodin tool

{{Short description|Modelling in Event-B}}
{{Infobox software
| title = Rodin
| name = 
| logo = <!-- File name without 'File:' -->
| logo caption = 
| logo alt = 
| logo size =
| collapsible = <!-- Any text here will collapse the screenshot. -->
| screenshot = <!-- File name without 'File:' -->
| screenshot size =
| screenshot alt = 
| caption = 
| other_names =
| author = [[Biography:Jean-Raymond Abrial|Jean-Raymond Abrial]], [[Biography:Michael Butler (computer scientist)|Michael Butler]], et al.
| developer = European Union Projects:
* RODIN (2004–2007)
* DEPLOY (2008–2012)
* ADVANCE (2011–2014)
| released = 2007<!-- {{Start date and age|YYYY|MM|DD|df=yes/no}} -->
| ver layout = <!-- simple (default) or stacked -->
| discontinued = <!-- Set to yes, if software is discontinued, otherwise omit. -->
| latest release version = 
| latest release date = <!-- {{Start date and age|YYYY|MM|DD|df=yes/no}} -->
| latest preview version = 
| latest preview date = <!-- {{Start date and age|YYYY|MM|DD|df=yes/no}} -->
| repo = <!-- {{URL|example.org}} -->
| qid = 
| programming language = [[Java (programming language)|Java]]
| middleware =
| engine = <!-- or |engines= -->
| operating system = 
| platform = [[Software:Eclipse|Eclipse]] IDE
| included with = 
| replaces =
| replaced_by =
| service_name = 
| size = 
| standard = 
| language = 
| language count = <!-- Number only -->
| language footnote = 
| genre = Software tool
| license = [[Open source]]
| website = {{URL|www.event-b.org}}
| AsOf = 
}}
The '''Rodin tool''' is a software tool for formal modelling in [[Event-B]].<ref name="abrial10">{{cite journal| author=Abrial, Jean-Raymond, Michael Butler, Stefan Hallerstede, Thai Son Hoang, Farhad Mehta, and Laurent Voisin. | title=Rodin: An open toolset for modelling and reasoning in Event-B | journal=International Journal on Software Tools for Technology Transfer | volume=12 | date=2010 | pages=447–466 | doi=10.1007/s10009-010-0145-y }}</ref><ref name="butler07">{{cite conference| author=Butler, Michael, and Stefan Hallerstede | title=The Rodin formal modelling tool | work=FACS 2007 Christmas Workshop: Formal Methods in Industry | pages=1–5 | date=2007 | url=https://www.scienceopen.com/document_file/c9c608d0-7377-4d50-8e7a-604d6c5c80dd/ScienceOpen/001_Butler.pdf }}</ref> It was developed as part of several collaborative [[Social:European Union|European Union]] projects, including initially the RODIN project (2004–2007).<ref>{{cite web| url=http://rodin.cs.ncl.ac.uk/ | title=RODIN: Rigorous Open Development Environment for Complex Systems | publisher=[[Organization:Newcastle University|Newcastle University]] | location=UK | accessdate=13 June 2023 }}</ref>

==Overview==
Event-B is a notation and method developed from the [[B-Method]] and is intended to be used with an incremental style of [[Modeling language|modelling]]. The idea of incremental modelling has been taken from programming: [[High-level programming language|modern programming languages]] come with [[Integrated development environment|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.<ref name="butler07" />

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|wiki]].<ref>{{cite web| url=http://wiki.event-b.org/ | title=Event-B and Rodin Documentation Wiki | website=wiki.event-b.org | accessdate=13 June 2023 }}</ref>

Rodin ("Rigorous Open Development Environment for Complex Systems") is an extension of [[Software:Eclipse|Eclipse]] IDE ([[Java (programming language)|Java]]-based). The Rodin Eclipse Builder manages the following:<ref>{{cite web| first=Michael | last=Butler |  url=https://www.southampton.ac.uk/~mbutler/rodin.pdf | title=RODIN – the next generation refinement tools | publisher=[[Organization:University of Southampton|University of Southampton]] | location=UK | accessdate=13 June 2023 }}</ref>

*Well-formedness and type checker
*Proof obligation (PO) generator
*Proof manager (PM)
*Propagation of changes

;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==
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.<ref>{{cite web| url=http://rodin.cs.ncl.ac.uk/D34.pdf | title=Project IST-511599 RODIN “Rigorous Open Development Environment for Complex Systems” | publisher=[[Organization:Newcastle University|Newcastle University]] | location=UK | accessdate=13 June 2023 }}</ref> 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==
*B4free provers<ref>{{cite web| url=https://www.clearsy.com/en/computer-science/b4free-as-a-free-fo-all-tool/ | title=B4free as a free-fo-all tool | publisher=ClearSy | accessdate=13 June 2023 }}</ref>
**Provider: ClearSy
**Function: Theorem provers
*UML-B<ref>{{cite web| url=https://www.uml-b.org/ | title=UML-B: Dependable Systems Modelling Language | website=uml-b.org | accessdate=13 June 2023 }}</ref>
**Provider: [[Organization:University of Southampton|University of Southampton]]
**Function: UML-like graphical front-end for Event-B supporting class diagrams and state charts
*ProB<ref>{{cite web| url=https://prob.hhu.de/ | title=What is ProB? | website=prob.hhu.de | publisher=[[Organization:University of Düsseldorf|University of Düsseldorf]] | location=Germany | accessdate=13 June 2023 }}</ref><ref>{{cite journal| author=Leonova, Mariya Aleksandrovna, and Petr Nikolaevich Devyanin | title=Comparison of methods for modeling access control in OS and DBMS in Event-B for the purpose of their verification with Rodin and ProB tools | journal=Prikladnaya Diskretnaya Matematika | volume=Supplement 15 | date=2022 | pages=90–99 | doi=10.17223/2226308X/15/22 }}</ref>
**Provider: [[Organization:University of Düsseldorf|University of Düsseldorf]]
**Function: Animation and Model-checking of Event-B models; Counterexamples for false proof goals, in particular, proof obligations
*Brama<ref>{{cite web| url=https://www.researchgate.net/publication/224195360_Domain_Engineering_with_Event-B_Some_Lessons_We_Learned/figures?lo=1 | title=The Brama animator for RODIN | website=ResearchGate.net | accessdate=13 June 2023 }}</ref>
**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<ref>{{cite web| url=http://wiki.event-b.org/index.php/Modularisation_Plug-in | title=Modularisation Plug-in | website=wiki.event-b.org | accessdate=13 June 2023 }}</ref>
**Provider: [[Organization:Newcastle University|Newcastle University]]
**Function: Structuring Event-B developments into logical units of modelling, called modules; Model composition; Model reuse

==References==
{{reflist}}

==Further reading==
*[[Biography:Jean-Raymond Abrial|Jean-Raymond Abrial]]. ''The B-Book: Assigning Programs to Meanings''. {{wipe|Cambridge University Press}}, 1996, ({{ISBN|0-521-49619-5}}).
*[[Biography:Jean-Raymond Abrial|Jean-Raymond Abrial]], [[Biography:Michael Butler (computer scientist)|Michael Butler]], Stefan Hallerstede, and Laurent Voisin. An open extensible tool environment for Event-B. In [[Biography:Zhiming Liu (computer scientist)|Z. Liu]] and [[Biography:He Jifeng|J. He]], editors, ''ICFEM 2006'', LNCS, volume 4260, pages 588–605. Springer, 2006.
*Abdolbaghi Rezazadeh, Neil Evans, and Michael Butler. Redevelopment of an Industrial, Case Study Using Event-B and Rodin. In ''BCS-FACS Christmas 2007 Meeting'', 2007.
*[http://rodin.cs.ncl.ac.uk/D18.pdf RODIN. Deliverable D18: Intermediate report on case study developments.]
*Michael Butler and Stefan Hallerstede, [http://deploy-eprints.ecs.soton.ac.uk/4/1/eventb.pdf The Rodin Formal Modelling Tool], EU Research Project IST 511599 RODIN.
*[http://www.eclipse.org/ Eclipse] platform homepage.

==External links==
* [http://www.event-b.org/ Event-B and the Rodin Platform]
* [http://wiki.event-b.org/ Event-B and Rodin Documentation Wiki]
* [https://sourceforge.net/projects/rodin-b-sharp/ Rodin] on [[Software:SourceForge|SourceForge]]

[[Category:Formal specification languages]]

{{Sourceattribution|Rodin tool|1}}