Enhancing EventB and RODIN: EventB-Rodin-Plus – EBRP-EventB-Rodin-Plus

The development of complex (software-based) systems requires multi-view system modelling involving different scientific disciplines and skills. For instance, in the case of autonomous systems, modelling behaviours and interactions of different systems may require control theory concepts such as differential equations, communication protocols, resource allocation, access control rules, etc.

State-based formal methods have proved their efficiency in supporting the development of such systems. One of these successful methods is Event-B and its RODIN IDE at the heart of the EBRP project proposal.
Nowadays, Event-B and RODIN offer a
- modelling language with formal semantics based on set theory and first order logic allowing to design state-based models and express system properties, namely safety;
- built-in refinement operation for modelling decomposition/composition mechanisms, defining a stepwise development from an abstract model to a concrete one;
- proof system to discharge proof obligations generated from models.

Although Event-B and its RODIN platform offer capabilities to handle complex system models related to different engineering domain areas, it may require to model concepts that are not explicitly supported by core Event-B (e.g. real numbers, classes, communication protocols, process calculi, other logics, resource allocation, access control). Their formal definition requires starting from the core Event-B concepts (set theory, predicate logic, basic integer arithmetic). In Event-B, this modelling chain is cumbersome and reuse of obtained models can be difficult.

The scientific challenge of EBRP is to address the Event-B development of complex systems allowing system models to define and borrow concepts from domain theories as first class citizens and to support formal reasoning on these objects.

To achieve this objective, EBRP pushes the idea of defining a framework for extending Event-B and RODIN with domain theories (and explicit import/export mechanisms) formalising the various domain concepts. In addition, the soundness of this extension will be established.
This extension framework shall allow developers to define/instantiate/import/ export/extend theories through the introduction of generic data types with associated operators, axioms and theorems. Moreover, this framework shall not be an adhoc one specifically designed for particular theories, but it will be generic. Finally, it will offer the capability for checking the correct use of these theories; in particular, it will address the soundness of mixing several theories together and the correctness of the obtained proofs.

EBRP is organised around 4 technical tasks dealing with the definition of domain theories, their use in formal models, their use in (automated) proofs and a validation of the approach through complex case studies of various themes (continuous/discrete).
The consortium of EBRP is made of experts of the Event-B method in France and in Europe. The inventor of the B and Event-B methods, Jean-Raymond Abrial, has accepted to join the EBRP project.