Translating Event-B machines to Eiffel programs

TL;DR

This paper introduces a source-to-source translation method from Event-B models to Eiffel programs, allowing correctness proofs via Eiffel's Design-by-Contract while leveraging object-oriented features.

Contribution

It presents the first systematic mapping from Event-B to Eiffel, integrating formal correctness proofs with object-oriented programming.

Findings

Enables proof of system properties through Eiffel's Design-by-Contract.

Preserves all features of object-oriented programming in the translation.

Facilitates formal verification in practical software development.

Abstract

Formal modelling languages play a key role in the development of software since they enable users to prove correctness of system properties. However, there is still not a clear understanding on how to map a formal model to a specific programming language. In order to propose a solution, this paper presents a source-to-source mapping between Event- B models and Eiffel programs, therefore enabling the proof of correctness of certain system properties via Design-by-Contract (natively supported by Eiffel), while still making use of all features of O-O programming.

Equations

$$\begin{array}[]{ll}\begin{array}[]{l}\textsf{machine }M\textsf{ sees }C\\ \textsf{variables}\;v\\ \textsf{invariants}\;label\_inv:\;I(s,c,v)\\ \textsf{events}\\ \hskip 8.5359pt\textsf{event}\;initialisation\\ \hskip 14.22636pt\textsf{then}\>A(s,c,v)\>\textsf{end}\\ \hskip 8.5359pt\textsf{event}\;evt\\ \hskip 14.22636pt\textsf{any}\;x\\ \hskip 8.5359pt\textsf{where}\\ \hskip 14.22636ptlabel\_guard:\;G(s,c,v,x)\\ \hskip 8.5359pt\textsf{then}\\ \hskip 14.22636ptlabel\_action:\;A(s,c,v,x)\\ \hskip 8.5359pt\textsf{end}\\ \textsf{end}\end{array}&\begin{array}[]{l}\textsf{Context }\;C\\ \textsf{constant}\;c\\ \textsf{set}\;S\\ \textsf{axioms}\;X(s,c)\\ \textsf{end}\end{array}\end{array}$$

$$\begin{array}[]{l}{\color[rgb]{0,0,0.5}{\bf class}}\;\textsf{ACCOUNT}\;{\color[rgb]{0,0,0.5}{\bf create}}\;\textsf{make}\\ {\color[rgb]{0,0,0.5}{\bf feature}}~{}{\color[rgb]{0.69921875,0.1328125,0.1328125}{-}{-}~{}\textsf{ Initalisation}}\\ \hskip 8.5359pt\textsf{make}\\ \hskip 25.6073pt~{}{\color[rgb]{0.69921875,0.1328125,0.1328125}{-}{-}~{}\textsf{Initialise an empty account.}}\\ \hskip 17.07182pt{\color[rgb]{0,0,0.5}{\bf do}}\\ \hskip 25.6073pt\textsf{balance := 0}\\ \hskip 17.07182pt{\color[rgb]{0,0,0.5}{\bf ensure}}\\ \hskip 25.6073pt{\color[rgb]{0,0,1}\text{balance\_set: }}\textsf{balance = 0}\\ \hskip 17.07182pt{\color[rgb]{0,0,0.5}{\bf end}}\\ {\color[rgb]{0,0,0.5}{\bf feature}}~{}{\color[rgb]{0.69921875,0.1328125,0.1328125}{-}{-}~{}\textsf{ Access}}\\ \hskip 8.5359pt\textsf{balance: INTEGER}\\ \hskip 17.07182pt~{}{\color[rgb]{0.69921875,0.1328125,0.1328125}{-}{-}~{}\textsf{Balance of this account.}}\\ {\color[rgb]{0,0,0.5}{\bf feature}}~{}{\color[rgb]{0.69921875,0.1328125,0.1328125}{-}{-}~{}\textsf{ Element change}}\\ \hskip 8.5359pt\textsf{withdraw (amount: INTEGER)}\\ \hskip 25.6073pt~{}{\color[rgb]{0.69921875,0.1328125,0.1328125}{-}{-}~{}\textsf{Withdraw `amount' from this account.}}\\ \hskip 17.07182pt{\color[rgb]{0,0,0.5}{\bf require}}\\ \hskip 25.6073pt{\color[rgb]{0,0,1}\text{amount\_not\_negative: }}\textsf{amount $>=$ 0}\\ \hskip 25.6073pt{\color[rgb]{0,0,1}\text{amount\_available: }}\textsf{amount $<=$ balance}\\ \hskip 17.07182pt{\color[rgb]{0,0,0.5}{\bf do}}\\ \hskip 25.6073pt\textsf{balance := balance - amount}\\ \hskip 17.07182pt{\color[rgb]{0,0,0.5}{\bf ensure}}\\ \hskip 25.6073pt{\color[rgb]{0,0,1}\text{balance\_set: }}\textsf{balance = {\color[rgb]{0,0,0.5}{\bf old}} balance - amount}\\ \hskip 17.07182pt{\color[rgb]{0,0,0.5}{\bf end}}\\ {\color[rgb]{0,0,0.5}{\bf invariant}}\\ \hskip 8.5359pt{\color[rgb]{0,0,1}\text{balance\_not\_negative: }}\textsf{balance $>=$ 0}\\ {\color[rgb]{0,0,0.5}{\bf end}}\end{array}$$

$$\displaystyle\penalty 1\begin{array}[]{lll}\textsf{$\tau$}\textsf{(}{v}\textsf{)}=\texttt{Type}&\textsf{$\xi$}\textsf{(}{I(s,c,v)}\textsf{)}=\texttt{Inv}&\textsf{$\delta$}\textsf{(}{\textsf{events}\>e}\textsf{)}=\texttt{E}\\ \lx@intercol\textsf{$\delta$}\textsf{(}{\textsf{event}\ initialisation\>\textsf{then}\>A(s,c,v)\>\textsf{end}}\textsf{)}=\texttt{Init}\hfil\lx@intercol\\ \end{array}$$

$$\displaystyle\penalty 1\begin{array}[]{ll}\textsf{$\delta$}\textsf{(}{\textsf{axioms}\;X(s,c)}\textsf{)}=\texttt{X}\\ \textsf{$\tau$}\textsf{(}{c}\textsf{)}=\texttt{Type}\end{array}$$

$$\displaystyle\penalty 1\begin{array}[]{ll}\textsf{$\tau$}\textsf{(}{s}\textsf{)}=\texttt{Type}\end{array}$$

$$\displaystyle\penalty 1\begin{array}[]{ll}\textsf{$\xi$}\textsf{(}{G(s,c,v,x)}\textsf{)}=\texttt{G}&\textsf{$\xi$}\textsf{(}{A(s,c,v,x)}\textsf{)}=\texttt{A}\\ \textsf{$\tau$}\textsf{(}{x}\textsf{)}=\texttt{Type}\end{array}$$

$$\displaystyle\penalty 1\begin{array}[]{ll}\textsf{$\xi$}\textsf{(}{A(s,c,v)}\textsf{)}=\texttt{A}\\ \end{array}$$

$$\begin{array}[]{ll}\begin{array}[]{l}\textsf{machine}\;m0\;\textsf{sees}\;c0\\ \textsf{variables}\;n\\ \textsf{invariants}\\ \hskip 14.22636pt\textsf{\bf{inv1: }}n\in\mathord{\mathbb{N}}\\ \hskip 14.22636pt\textsf{\bf{inv2: }}n\leq d\\ \textsf{events}\\ \hskip 14.22636pt\textsf{event }INITIALISATION\\ \hskip 28.45274pt\textsf{then}\\ \hskip 42.67912pt\textsf{\bf{act1 }}n:=0\\ \hskip 14.22636pt\textsf{end}\\ \hskip 14.22636pt\textsf{event }ML\_out\\ \hskip 28.45274pt\textsf{where}\\ \hskip 42.67912pt\textsf{\bf{grd1 }}n<d\\ \hskip 28.45274pt\textsf{then}\\ \hskip 42.67912pt\textsf{\bf{act1 }}n:=n+1\\ \hskip 14.22636pt\textsf{end}\\ \hskip 14.22636pt\textsf{event }ML\_in\\ \hskip 28.45274pt\textsf{where}\\ \hskip 42.67912pt\textsf{\bf{grd1 }}n>0\\ \hskip 28.45274pt\textsf{then}\\ \hskip 42.67912pt\textsf{\bf{act1 }}n:=n-1\\ \hskip 14.22636pt\textsf{end}\\ \textsf{end}\\ \end{array}&\begin{array}[]{l}\textsf{context }c0\\ \textsf{constants }d\\ \textsf{axioms}\\ \hskip 14.22636pt\textsf{\bf{axm1 }}d\in\mathord{\mathbb{N}}\\ \hskip 14.22636pt\textsf{\bf{axm2 }}d>0\\ \textsf{end}\end{array}\end{array}$$

$$\begin{array}[]{ll}\begin{array}[]{l}{\color[rgb]{0,0,0.5}{\bf class}}\;\textsf{m0}\;{\color[rgb]{0,0,0.5}{\bf create}}\;\textsf{INITIALISATION}\\ {\color[rgb]{0,0,0.5}{\bf feature}}~{}{\color[rgb]{0.69921875,0.1328125,0.1328125}{-}{-}~{}\textsf{ Initalisation}}\\ \hskip 8.5359pt\textsf{initialisation}\\ \hskip 17.07182pt{\color[rgb]{0,0,0.5}{\bf do}}\\ \hskip 25.6073pt{\color[rgb]{0,0,0.5}{\bf create}}\;\textsf{ctx}\\ \hskip 25.6073pt\textsf{n := 0}\\ \hskip 17.07182pt{\color[rgb]{0,0,0.5}{\bf ensure}}\\ \hskip 25.6073pt{\color[rgb]{0,0,1}\text{act1: }}\textsf{n = 0}\\ \hskip 17.07182pt{\color[rgb]{0,0,0.5}{\bf end}}\\ {\color[rgb]{0,0,0.5}{\bf feature}}~{}{\color[rgb]{0.69921875,0.1328125,0.1328125}{-}{-}~{}\textsf{ Events}}\\ \hskip 8.5359pt\textsf{ml\_out}\\ \hskip 17.07182pt{\color[rgb]{0,0,0.5}{\bf require}}\\ \hskip 25.6073pt{\color[rgb]{0,0,1}\text{grd1: }}\textsf{n $<$ d}\\ \hskip 17.07182pt{\color[rgb]{0,0,0.5}{\bf do}}\\ \hskip 25.6073pt\textsf{n := n + 1}\\ \hskip 17.07182pt{\color[rgb]{0,0,0.5}{\bf ensure}}\\ \hskip 25.6073pt{\color[rgb]{0,0,1}\text{act1: }}\textsf{n = {\color[rgb]{0,0,0.5}{\bf old}} n + 1}\\ \hskip 17.07182pt{\color[rgb]{0,0,0.5}{\bf end}}\end{array}&\begin{array}[]{l}\hskip 8.5359pt\textsf{ml\_in}\\ \hskip 17.07182pt{\color[rgb]{0,0,0.5}{\bf require}}\\ \hskip 25.6073pt{\color[rgb]{0,0,1}\text{grd1: }}\textsf{n $>$ 0}\\ \hskip 17.07182pt{\color[rgb]{0,0,0.5}{\bf do}}\\ \hskip 25.6073pt\textsf{n := n - 1}\\ \hskip 17.07182pt{\color[rgb]{0,0,0.5}{\bf ensure}}\\ \hskip 25.6073pt{\color[rgb]{0,0,1}\text{act1: }}\textsf{n = {\color[rgb]{0,0,0.5}{\bf old}} n - 1}\\ \hskip 17.07182pt{\color[rgb]{0,0,0.5}{\bf end}}\\ {\color[rgb]{0,0,0.5}{\bf feature}}~{}{\color[rgb]{0.69921875,0.1328125,0.1328125}{-}{-}~{}\textsf{ Access}}\\ \hskip 8.5359pt{\color[rgb]{0,0,0.5}{\bf ctx:CONSTANTS}}\\ \hskip 8.5359pt{\color[rgb]{0,0,0.5}{\bf n:INTEGER}}\\ {\color[rgb]{0,0,0.5}{\bf invariant}}\\ \hskip 8.5359pt{\color[rgb]{0,0,1}\text{inv1: }}\textsf{n $>=$ 0}\\ \hskip 8.5359pt{\color[rgb]{0,0,1}\text{inv2: }}\textsf{n $<=$ d}\\ {\color[rgb]{0,0,0.5}{\bf end}}\end{array}\end{array}$$

Full text

Design-by-Contract, Stepwise refinement, Event-B, Eiffel

††conference: Conf.; 2017; ††copyright: none

1. Introduction

The importance of developing correct software systems has been increased in the past few years. Final users of systems trust systems and are not aware of the consequences of malfunctioning. Hence, the burden is on developers, engineers and researchers that have to pay close attention to the development of flawless systems. There are different approaches to tackle the problem, e.g. top-down and bottom-up approaches: using a top-down approach, one could think to start developing the system from a very abstract view point towards more concrete ones; in a bottom-up approach, on the other hand, one might think to start from a more concrete state of the system to then add more functionality to it. The key point on both approaches is to always prove that properties of the systems hold.

Event-B is a formal modelling language for reactive systems, introduced by Abrial (Abrial, 2010), which allows the modelling of complete systems. It follows the top-down approach by means of refinements. One can create an abstraction of the system and express its properties. Prove that the system indeed meets the properties to then create a refinement of the system: same system with more details. It has been applied with success in both research and industrial projects, and in integrated EU projects aiming at putting together the two dimensions, for example in the automotive sector (Gmehlich et al., 2013).

On the other side of the spectrum, following a bottom-up approach, one can work with Eiffel programming language (Meyer, 1992). In Eiffel, one can create classes that implement any system. The behaviour of such classes is specified in Eiffel using contracts: pre- and post-conditions and class invariants. These mechanisms are natively supported by the language. Having contracts, one can then verify that the implementation is indeed the intended. After the implementation of the class, one can give more speciality or generalization by using inheritance. This paper gives a series of rules to generate Eiffel programs from Event-B model, bridging both top-down and bottom-up approaches. Rules take into account system specifications of the Event-B model and generate either Eiffel code or contracts. Thus, users will end up with an implementation of the system while they can prove it correct.

Several translations have been achieved that go in the same direction as the work presented on this paper. In (Méry and Singh, 2011), Mèry and Singh present the EB2ALL tool-set that includes a translation from Event-B models to C, C++ and Java. Unlike this translation, EB2ALL provides support for a small part of Event-B’s syntax, and users are required to write a final Event-B implementation refinement in the syntax supported by the tool. The Code Generation tool (Edmunds and Butler, 2010) generates concurrent Java and Ada programs for a tasking extension of Event-B. Unlike these tools, the work presented here does not require user’s intervention, while it works on the proper syntax of the Event-B model. In addition, these tools do not take full advantage of the elements present in the source language, e.g. invariants. The work presented in this paper, in addition to an implementation, generates contracts from the source language, making use of the Design-by-Contract approach. In (Rivera et al., 2017; Cataño and Rivera, 2016), authors present a translation from Event-B to Java, annotating the code with JML (Java Modelling Language) specifications, and (Rivera et al., 2016) shows its application. The main difference with the work presented here is the target language. We are translating to Eiffel which natively supports Design-by-Contract. In addition, Eiffel comes with different tools to statically prove Eiffel code (e.g. Autoproof (Tschannen et al., 2015)) that fully supports the language. Another difference is the translation of carrier sets. EventB2Java translates them as set of integers

2. Preliminaries

2.1. Event-B

Event-B is a formal modelling language for reactive systems, introduced by Abrial (Abrial, 2010), which allows the modelling of complete systems. Figure 1 shows the general view of an Event-B machine and context. Event-B models are composed of contexts and machines. Contexts define constants (written after constant in context $C$), uninterpreted sets (written after set in context $C$) and their properties (written after axioms in context $C$). Machines define variables (written after variables in machine $M$) and their properties (expressed as invariants after invariant in machine $M$), and state transitions expressed as events (written between events and the last end). The initialisation event gives initial values to variables.

An event is composed of guards and actions. The guard (written between keywords where and then) represents conditions that must hold for the event to be triggered. The action (written between keywords then and end) gives new values to variables

In Event-B, systems are modelled via a sequence of refinements. First, an abstract machine is developed and verified to satisfy whatever correctness and safety properties are desired. Refinement machines are used to add more detail to the abstract machine until the model is sufficiently concrete for hand or automated translation to code. Refinement proof obligations are discharged to ensure that each refinement is a faithful model of the previous machine, so that all machines satisfy the correctness properties of the original.

2.2. Eiffel

Eiffel is an Object-Oriented programming language that natively supports the Design-by-Contract methodology. The behaviour of classes is specified by equipping them with contracts. Each routine of the class contains a pre- and post-condition: a client of a routine needs to guarantee the pre-condition on routine call. In return, the post-condition of the procedure, on routine exit, holds. The class is also equipped with class invariants. Invariants maintain the consistency of objects. Contracts in Eiffel follow a similar semantics of Hoare Triples.

Figure 2 depicts an Eiffel class that implements part of a Bank Account. The name of the class is ACCOUNT and it appears right after the keyword class. In Eiffel, implementers need to list creation procedures after the keyword create. In Figure 2, make is a procedure of the class that can be used as a creation procedure. Class ACCOUNT structures its procedures in Initialisation, Access and Element change, by using the keyword feature. This structure can be use for information hiding (not discussed here). balance is a class attribute that contains the actual balance of the account. It is defined as an integer. Procedures in Eiffel are defined by given them a name (e.g. withdraw) and its respective arguments. It is followed by a head comment (which is optional). Procedures are equipped with pre- and post-conditions predicates. In Eiffel, a predicate is composed of a tag (optional) and a boolean expression. For instance, the pre-condition for withdraw (after the key work require) imposes the restriction on callers to provide and argument that is greater than or equal zero and less than or equal the balance of the account (amount_not_negative and amount_available are tags, identifiers, and are optionals). If the pre-condition of the procedure is met, the post-condition (after the key work ensure) holds on procedure exit. In a post-condition, the aid old refers to the value of an expression on procedure entry. The actions of the procedure are listed in between the key words do and ensure. The only action of withdraw procedure is to increase the value of balance by amount. Finally, The invariant is restricting the possible values for variables.

3. Translation

The translation is done by the aid $\delta$ $:$ Event-B $\mathbin{\rightarrow}$ Eiffel. $\delta$ takes an Event-B model and produces Eiffel classes. It is defined as a total function (i.e. $\mathbin{\rightarrow}$) since any Event-B model can be translated to Eiffel. It uses two helpers: $\xi$ translates Event-B Expressions or Predicates to Eiffel, and $\tau$ translates the type of Event-B variable to the corresponding type in Eiffel.

3.1. Translating Event-B machines

Rule machine is a high level translation. It takes an Event-B machine M and produces an Eiffel class M.

[TABLE]

Variables are translated as class attributes in class M. Event-B invariants are translated to Eiffel invariants. Both, Event-B and Eiffel, have similar semantics for invariants. Rule context generate an Eiffel class CONSTANT that contains the translation of Event-B constants and carrier sets defined by the user. Axioms, which restrict the possible values for constants are translated to invariants of this class. Constants in Event-B are entities that cannot change their values. They are naturally translated to Eiffel as once variables.

[TABLE]

Carrier sets represent a new type defined by the user. Each carrier set is translated as an afresh Eiffel class so users are able to use them as types. Rule cset shows the translation. Parts of the class are omitted due to space. Class EBSET [T] gives an implementation to sets of type T. Class S inherits EBSET [T] due to the nature of carrier sets in Event-B.

[TABLE]

Rule event produces an Eiffel feature given an Event-B $event$. Parameters of the event are translated as arguments of the respective feature in Eiffel with its respective type. In Event-B, an event might be executed only if the guard is true. In Eiffel, the guard is translated as the precondition of the feature. Hence, the client is now in charge of meeting the specification before calling the feature. The semantics of the execution is handle now by the client who wants to execute the feature rather than the system deciding. The actual execution of the actions still preserve its semantics: execution of the actions is only possible if the guard is true. In Eiffel, for a client to execute a feature he needs to meet the guard otherwise a runtime exception will be raised: Contract violation.

Event-B event actions are translated directly to Eiffel statements. In Event-B, the before-after predicate contains primed and unprimed variables representing the before and after value of the variables. We translated the primed variable with the Eiffel key word old. Representing old value of the variable. For simplicity. the rule only takes into account a single parameter, a single guard and a single action. However, this can be easily extended.

[TABLE]

Rule init below shows the translation of Event-B event $initialisation$ to a creation procedure in Eiffel. The creation procedure initialises the object containing the constants definition. It also assigns initial values to variables taken from the initialisation in the $initialisation$ event. In Eiffel, creation procedures are listed under the keyword create, as shown in rule machine. The ensure clause shows the translation of the before-after predicate of the assignment in Event-B.

[TABLE]

3.2. Hand translation

In this Section, we apply (manually) the translation rules to the Event-B model in Figure 3. The Event-B model is a well known model created by Abrial in (Abrial, 2010). It models a system for controlling cars in an island and on a bridge. The model depicted in Figure 3 only shows the most abstract model of the system.

Machine $m0$ sees context $c0$. $c0$ defines a constant $d$ as a natural number greater than 0. This constant models the maximum number of cars that can be on the island and bridge. Machine $m0$ also defines a variable $n$ as a natural number (predicate inv1). Variable $n$ is the actual number of cars in the island and on the bridge. Predicate inv2 imposes the restriction on the number of cars, it must not be over $d$. Event $initialisation$ gives an initial value to $n$: no cars in the island or on the bridge. Event $ML\_out$ models the transition for a car in the mainland to enter the island. The restriction is that the number of cars already in the island is strictly less than $d$: there is room for at least another car. Its action is to increase the number of cars in the island by one. Event $ML\_in$ models the transition for a car in the island to enter the mainland. The only restriction is that there is at least one car in the island. Its action is to decrease the number of cars in the island. All these restrictions are ensured by the proof obligations.

Figure 4 is the mapping to Eiffel programming language by applying the rules in Section 3.

4. Conclusion

We presented a series of rules to transform an Event-B model to an Eiffel program. The translation takes full advantage of all elements in the source by translating them as contracts in the target language. Thus, no information on the behaviour of the system is lost. These rules shows a methodology for software construction that makes use of two different approaches.

We plan on implementing these rules as an Event-B plug-in. We also plan of taking full advantage of the Proof Obligations generated by Event-B: translated them into a specification driven class so to help Eiffel provers in the process of proving the correctness of classes after any modification (extension) done by the implementer.