EventB Rodin description

Presentation

Rodin

Website

http://www.event-b.org/

Contact email

[email protected]

http://www.event-b.org/contact.html (Rodin Community)

Main usage:

• Formal Modeling and Proof
• Formal Model verification
• Model Simulation

Summary

Rodin is an industrial strength formal modeling tool. It allows for the application of the Event-B approach to formal systems modeling. It provides proof obligation creation for invariants, refinement relations and data types. It comprises an Eclipse based modeling framework and supports numerous plugins, e.g., graphical modeling (iUML), automated proof support (theorem provers, SMT solvers) and traceability of requirements (ProR). It was developed by various academic and industrial partners in the European Union Projects RODIN (2003-2007), DEPLOY (2008-2012) and currently ADVANCE (2011-2014).

Publications

• Rodin Flyer http://sourceforge.net/projects/rodin-b-sharp/files/Doc_Rodin_General/Rodin_Leaflets/Leaflet_Rodin_E.pdf
• Rodin Handbook (2012): http://handbook.event-b.org

Support and Survivability

Rodin is open-source (EPL licence) available on source forge. Support can be provide by the mailing list : [email protected]

Applicability

Key capabilities

• Support for Event-B modeling and formal verification approach
• Iterative model development using model refinement
• Dynamic behaviour visualization through animation (AnimB, ProB, BMotion Studio) and simulation
• Connections to others languages (UML, SysML,...) via plugin
• Traceability facilities via plugin (ProR)
• Extension to external VnV tools via pluggin (solvers SMT, test generator, simulator,...)
• Full integration in the Eclipse Framework
• Extensive plugin support

Input

• Event-B formal language
• via plugins: graphical modeling
  • state machines
  • UML-B class diagrams

Output (Proof, code, other)

• Proofs - proof trees
• graphical model representations
• model / requirements traceability

Main restrictions

• proof support for non-linear arithmetic and hybrid systems is currently limited (both are ongoing research projects)

Manual or automated use of the tool

• manual tasks
  • textual modeling in Event-B
  • graphical modeling using state machines
• automated tasks
  • large part of proof obligations (~ 99% for industrial case studies, see "SMT Solvers for Rodin" at ABZ 2012 conference)

Expertise level

• basic knowledge of mathematical logic

Integration in the tool chain

Currently distributed: Yes

Underlying technologies

• Platform: Eclipse, EMF
• Implementation Language: Java
• Requirements:
  • Java 1.6
  • Platform: Eclipse 3.7
  • OS: Linux (32/64 Bit), Windows (32/64 Bit), MacOS X (64 Bit)

Traceability

• Traceability between source requirements and formal model is possible via the ProR pluggin

Team work:

• Egit pluggin or SVN pluggin can be used with Rodin
• A pluggin is dedicaded to the team management using SVN tool
• Extension to improve team management are planned

Certification issues:

In an industrial usage, Rodin is proposed to support system design activity. In such context, rodin is expected to be a T1 class tool as defined in EN50128.

Participators

• ADVANCE project - coordinator: Dr John Colley ([email protected])
  • University of Southampton, UK
  • Alstom Transport, France
  • Systerel, France
  • Heinrich-Heine University of Düsseldorf, Germany
  • Critical Software Technologies Ltd, UK
• DEPLOY project - coordinator: Prof. Alexander Romanovsky ([email protected])
  • CETIC, Belgium
  • Systerel, France
  • ClearSy, France
  • Åbo Akademi University, Finland
  • Bucharest University, Romania
  • University of Newcastle upon Tyne, UK
  • University of Southampton, UK
  • Piteşti University, Romania
  • Heinrich-Heine University of Düsseldorf, Germany
  • Swiss Federal Institute of Technology in Zürich - ETHZ, Switzerland
  • Bosch, Germany
  • Siemens Transportation Systems, Germany
  • Space Systems Finland, Finland
  • SAP, Germany
• RODIN project - coordinator: Prof. Alexander Romanovsky ([email protected])
  • University of Newcastle upon Tyne, UK
  • Åbo Akademi University, Finland
  • Swiss Federal Institute of Technology in Zürich - ETHZ, Switzerland
  • University of Southampton, UK
  • Praxis High Integrity Systems Ltd, UK
  • Nokia Corporation, Finland
  • ClearSy, France
  • AT Engine Controls Ltd, UK

stable or recommended version of the tool

• current stable version: Rodin 2.7

Tool available for openETCS participants?

Yes

If yes, Under which licence?

• Eclipse Public License

Licenses of underlying technologies

• plugins may have different licenses, necessary plugins are at least freely available

Eclipse interface

• full integration into Eclipse

Other integration possibilities

• easy integration in any Eclipse based tool
• e.g., IMOFIS ALEA toolkit (integration of Rodin and topCased in Obeo Designer)

Existing industrial usage

• NTT-Data, Fujitsu, Hitachi, NEC, Toshiba, and SCSK (DSF group) - found advantages of the Event-B approach compared with traditional development
• Bosch - cruise control system and a start-stop system
• Siemens Transportation - train control and signalling systems
• Space Systems Finland - BepiColombo space probe and on Attitude and Orbit Control System software (AOCS)
• SAP - analysis of business choreography models
• Systerel
  • DIR 41 case study: specification of a computerized interlocking
  • analysis of the interface between two zones of a CBTC system
  • Specification of a zone controller of a CBTC system (automatic metro)
  • Formal Data Validation
• Newcastle University - SafeCap: modelling techniques and tools for improving railway capacity while ensuring that safety standards
• AeS Group - several projects in railway domain
• XMOS Ltd - Instruction Set Architecture Definition of the XCore Microprocessor
• QNX Software Systems Limited - design of software for a simple medical device

for more details see also http://wiki.event-b.org/index.php/Industrial_Projects

Planned development

details are given here