About EBRP

The purpose of this project is to enhance Event-B and the corresponding RODIN toolset. This will be done by engaging in some basic research dealing with various mathematical theories that are not currently available in Event-B and RODIN.

The development of complex (software-based) systems usually requires multi-view modelling when the systems involve 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.

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 to formalise system properties,
  • built-in refinement operation allowing to define model, with decomposition/composition mechanisms,
  • proof system to discharge the proof obligations generated for each model.

Although Event-B and RODIN support complex system development, handling complex models related to different engineering domain areas [?] may require to model concepts that are not explicitly available nor supported by core Event-B. Examples of such concepts are reals and continuous functions, classes, and more generally new types with associated operators and properties. Their formal definitions require to start from the core Event-B concepts i.e. from set theory, predicate logic and basic arithmetic. This modelling chain is possible with Event-B but it is cumbersome and makes the proof difficult to carry, because of all the details of the encoding in set theory. Moreover, reuse of the obtained models is not directly possible. The Theory plug-in in RODIN has been developed to overcome these difficulties, but the first version of this plugin was a proof of concept developed by a PhD student and it needs a major overhaul to become practically viable and theoretically sound.

EBRP targets the definition of extension mechanisms for Event-B rather than defining domain specific modelling languages. The extension of Event-B to support complex system developments requiring the modelling of complex mathematical objects and the support of associated proofs is still a research challenge.

Allowing Event-B models to import and use externally defined domain theories is supported by the Theory construct of Event-B defined in a previously and implemented in RODIN as a Plug-in. The possibility to specify, within a domain theory, such complex mathematical objects becomes possible using this Theory construct and domain specific concepts related to the domain theory become explicitly defined in models and manipulated using operators defined in this theory.

However, the main focus of EBRP is to address the following issues:

  • Building a sound mechanism to import specific domain theories or instantiated generic ones. This one should allow importing complex data types to be used in the modelling language together with all the mathematical justifications ensuring their sound importation and use. All the operators, properties (axioms and theorems) and proof rules available in these theories will be made available in the Event-B models for complex systems modelling purpose.
  • Handling the semantic heterogeneity resulting from the integration (extension) of different theories. Contradictory axioms and soundness issues may occur. Extension and integration of theories to build more complex theories shall lead to correct theory importation proof obligations.
  • Similarly to the previous issue, importation of various theories in Event-B models may lead to similar problems. Importation of theories in Event-B models shall lead to correct theory importation proof obligations.
  • Regarding the verification of the defined and imported theories, it is important to offer a proof system to support the proof of correctness of these theories. Moreover, it is suited to use various proof systems well adapted for specific forms of proof obligations. In this case, heterogeneous proofs may appear due to the use of different proof systems and therefore proof certification issues should be addressed. In particular, moving from axiomatic theories to constructive theories for proof purposes is a key issue.
  • Finally, the RODIN tool shall be improved in order to support both theory definition, importation and use in Event-B models and various proof engines together with the possibility to produce proof certificates.