Tools, methods, and applications of Event-B

European Framework V IST project RODIN (Rigorous Open Development Environment for Complex Systems) aims at

"the creation of a methodology and supporting open tool platform for the cost effective rigorous development of dependable complex software systems and services"

The project is developing the second generation of the leading model-based formal method, B, created by Jean-Raymond Abrial. The language is known as Event-B, emphasising the incorporation of an event perspective. The project will produce a mature open-source toolset for Event-B; prototypes are now available at

Using the practical experience of the specification and development of four industrial case studies with industrial partners, rich methodology for formal development will be produced, for general and domain-specific usage. One of the case studies (see RODIN deliverable D4), a failure management system for engine control, has a generic character; that is, it should be deployable in various different airframes. Thus while considering the failure management domain (an important topic in control engineering), we will be concerned with various forms of software reuse, such as component engineering, and software product line engineering. Feature-based specification and refinement are topics of particular interest. Specification work includes the application of UML-B, a UML-front-end tool for Event-B.

Research and project work is available.

Updated 30/4/06