# An Institution for Event-B

Marie Farrell, Rosemary Monahan, James F. Power

► To cite this version:

Marie Farrell, Rosemary Monahan, James F. Power. An Institution for Event-B. 23th International Workshop on Algebraic Development Techniques (WADT), Sep 2016, Gregynog, United Kingdom. pp.104-119, 10.1007/978-3-319-72044-9_8. hal-01767469

HAL Id: hal-01767469

https://inria.hal.science/hal-01767469

Submitted on 16 Apr 2018

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# An Institution for Event-B

Marie Farrell*, Rosemary Monahan, and James F. Power

Dept. of Computer Science, Maynooth University, Co. Kildare, Ireland

**Abstract.** This paper presents a formalisation of the Event-B formal specification language in terms of the theory of institutions. The main objective of this paper is to provide: (1) a mathematically sound semantics and (2) modularisation constructs for Event-B using the specification-building operations of the theory of institutions. Many formalisms have been improved in this way and our aim is thus to define an appropriate institution for Event-B, which we call $EVT$. We provide a definition of $EVT$ and the proof of its satisfaction condition. A motivating example of a traffic-light simulation is presented to illustrate our approach.

**Keywords:** Event-B; institutions; refinement; formal methods; modular specification; formal specification

## 1 Introduction and Motivation

Event-B is an industrial-strength, state-based formalism for system-level modelling and verification, combining set theoretic notation with event-driven modelling. However, Event-B lacks well-developed modularisation constructs and it is not easy to combine specifications in Event-B with those written in other formalisms [6]. Our thesis, presented in this paper, is that the theory of institutions can provide a framework for defining a rich set of modularisation operations and promoting interoperability and heterogeneity for Event-B.

This paper is centered around an illustrative example of a specification written in Event-B, inspired by one in the *Rodin Handbook* [7], which we present in the remainder of Section 1. We define our institution for Event-B, called $EVT$, in Section 2, prove that it is a valid institution, and define a comorphism between the institution for first-order predicate logic with equality and $EVT$ in Section 3. In Section 4 we use this institution to recast our Event-B example in modular form using specification-building operators and address refinement, since this is of central importance in Event-B. We summarise our contributions and outline future directions in Section 5.

### 1.1 Formal Specification of a Traffic-Lights System in Event-B

Figure 1 presents an Event-B machine for a traffic-lights system with one light signalling cars and one signalling pedestrians [2]. The goal of the specification

<footnote>* This work is funded by Government of Ireland Postgraduate Grant from the Irish Research Council.</footnote>
is to ensure that it is never the case that both cars and pedestrians receive the "go" signal at the same time (represented by boolean flags on line 2). Machine specifications typically contain variable declarations (line 2), a variant expression (none in this example), invariants (lines 3-6) and event specifications (lines 7-21). *Contexts* in Event-B can be used to model the static properties of a system (constants, axioms and carrier sets). Figure 2 provides a context giving a specification for the data-type *COLOURS*. The axiom on line 5 explicitly restricts the set to only contain the constants *red*, *green* and *orange*.

Figure 1 specifies five different events (including a starting event called *Init-ialisation* defined on lines 8–10). Each event has a guard, specifying when it can be activated, and an action, specifying what happens when the event is activated. For example, the *set-peds-go* event as specified on lines 11–13, has one guard expressed as a boolean expression (line 12), and one action, expressed as an assignment statement (line 13). Moreover, each event has a status, which can be either *ordinary*, *convergent*, or *anticipated*. If the status is different from *ordinary*, then the event is concerned with the variant expression, i.e. with a natural-number expression used in proving termination properties. Our example has no variant so all events have the status *ordinary*.

Figure 3 shows an Event-B machine specification for mac2 that refines the machine mac1 (Figure 1). The machine mac1 is refined by first introducing the new context on line 1 and then by replacing the truth values used in the abstract machine with new values from the carrier set COLOURS. This new data type is included into mac2 using the SEES construct on line 1 of Figure 3. During refinement, the user typically supplies a *gluing invariant* relating properties of the abstract machine to their counterparts in the concrete machine [2]. The gluing invariants in Figure 3 (lines 6 and 8) define a one-to-one mapping between the concrete variables introduced in mac2 and the abstract variables of mac1. The concrete variables (*peds[*colour* and *cars[*colour*]*) can be assigned either *red* or *green*, thus the gluing invariants map *true* to *green* and *false* to *red*.

Event-B permits the addition of new variables and events: *button_pushed* (line 2) and *press_button* (lines 30–31). The existing events from mac1 are renamed to reflect refinement; for example, the event *set-peds-green* is declared to refine *set-peds-go* (lines 14–15). This event has also been altered via the addition of a guard (line 16) and an action (line 18) that incorporate the functionality of a button-controlled pedestrian light. This example highlights features of the Event-B language, but notice how the same specification has to be provided twice in Figure 1. The events *set-peds-go* and *set-peds-stop* are equivalent, modulo renaming of variables, to *set-cars-go* and *set-cars-stop*. Ideally, writing and proving the specification for these events should only be required once. Our approach addresses these issues as will be seen in Section 4.

## 1.2 Related Work: Institutions and Modularisation

Originally, Event-B was not equipped with any modularisation constructs. Because of this, several approaches have been suggested for modularising Event-B
1 MACHINE mac1
2 VARIABLES cars-go, peds-go
3 INVARIANTS
4 inv1: cars-go ∈ BOOL
5 inv2: peds-go ∈ BOOL
6 inv3: ¬ (peds-go = true
  ∧ cars-go = true)
7 EVENTS
8 Initialisation ordinary
9 then act1: cars-go ::= false
10 act2: peds-go ::= false
11 Event set.peds.go = ordinary
12 when grd1: cars-go = false
13 then act1: peds-go ::= true
14 Event set.peds.stop = ordinary
15 then act1: peds.go ::= false
16 Event set.cars.go = ordinary
17 when grd1: peds-go = false
18 then act1: cars-go ::= true
19 Event set.cars.stop = ordinary
20 then act1: cars.go ::= false
21 END

<caption>Fig. 1: Event-B machine specification for a traffic system.</caption>

1 CONTEXT ctx1
2 SETS COLOURS
3 CONSTANTS red, green, orange
4 AXIOMS
5 axm1: partition(COLOURS,
  {red}, {green}, {orange})
6 END

<caption>Fig. 2: Event-B context specification for the colours of a set of traffic-lights.</caption>

1 MACHINE mac2 refines mac1 SEES ctx1
2 VARIABLES cars-colour, peds-colour,
  buttonpushed
3 INVARIANTS
4 inv1: peds-colour ∈ {red, green}
5 inv2: (peds-go = true) ⇔ (peds-colour = green)
6 inv3: cars-colour ∈ {red, green}
7 inv4: (cars-go = true) ⇔ (cars-colour = green)
8 inv5: buttonpushed ∈ BOOL
9 EVENTS
10 Initialisation ordinary
11 then act1: cars-colour ::= red
12 act2: peds-colour ::= red
13 Event set.peds.green = ordinary
14 refines set.peds.go
15 when grd1: cars-colour = red
16 grd2: buttonpushed = true
17 then act1: peds-colour ::= green
18 then act2: buttonpushed ::= false
19 Event set.peds.red = ordinary
20 refines set.peds.stop
21 then act1: peds-colour ::= red
22 Event set.cars.green = ordinary
23 refines set.cars.go
24 when grd1: peds.colour = red
25 then act1: cars-colour ::= green
26 Event set.cars.red = ordinary
27 refines set.cars.stop
28 then act1: cars-colour ::= red
29 Event press.button = ordinary
30 then act1: buttonpushed ::= true
31 END

<caption>Fig. 3: A refined Event-B machine specification for a traffic system.</caption>

specifications. Abrial first proposed two styles of decomposition based on identifying shared variables and shared events [3]. Elaborating these approaches, approximately 8 modularisation plugins have been developed for various versions of Rodin, each offering a different perspective on implementing modularisation. By defining an institution for the Event-B formalism, we can modularise Event-B specifications using specification-building operators [11], and thus provide an approach to developing modular specifications that is consistent with the state of the art in formal specification.

An attempt was previously made to provide an institution and corresponding morphisms for Event-B and UML [4]. However, the definitions of Event-B sentences and models were vague, making it difficult to evaluate their semantics in a meaningful way. Also, the models described resemble the set-theoretic foundations of B specifications, whereas here we concentrate on event-based models. Our presentation of an illustrative example in both Event-B and its modular institutional version is an important element of developing this work.

Our approach provides scope for the interoperability of Event-B and other formalisms via institution (co)morphisms. Those familiar with the institution for UML state machines, UML, may notice that we have based the construction of
our institution for Event-B, $\mathcal{EVT}$, on $\mathcal{UML}$[8]. Both institutions describe state-based formalisms so, by keeping $\mathcal{UML}$ in mind during the development of $\mathcal{EVT}$, it will be possible to design meaningful translations between them in the future.

## 2 An Institution for Event-B

The theory of institutions, originally developed by Goguen and Burstall in a series of papers originating from their work on algebraic specification, provides a general framework for defining a logical system [5].

**Definition 1 (Institution).** An institution $\mathcal{INS}$ for some given formalism will consist of definitions for:

**Vocabulary:** a category **Sign** whose objects are called signatures and whose arrows are called signature morphisms.

**Syntax:** a functor $\mathbf{Sen} : \mathbf{Sign} \to \mathbf{Set}$ giving a set $\mathbf{Sen}(\Sigma)$ of $\Sigma$-sentences for each signature $\Sigma$ and a function $\mathbf{Sen}(\sigma) : \mathbf{Sen}(\Sigma) \to \mathbf{Sen}(\Sigma')$ for each signature morphism $\sigma : \Sigma \to \Sigma'$.

**Semantics:** a functor $\mathbf{Mod} : \mathbf{Sign}^{op} \to \mathbf{Cat}$ giving a category $\mathbf{Mod}(\Sigma)$ of $\Sigma$-models for each signature $\Sigma$ and a functor $\mathbf{Mod}(\sigma) : \mathbf{Mod}(\Sigma') \to \mathbf{Mod}(\Sigma)$ for each signature morphism $\sigma : \Sigma \to \Sigma'$.

**Satisfaction:** for every signature $\Sigma$, a satisfaction relation $\models_{\mathcal{INS},\Sigma}$ between $\Sigma$-models and $\Sigma$-sentences.

An institution must uphold the **satisfaction condition:** for any signature morphism $\sigma : \Sigma \to \Sigma'$ and translations $\mathbf{Mod}(\sigma)$ of models and $\mathbf{Sen}(\sigma)$ of sentences we have for any $\phi \in \mathbf{Sen}(\Sigma)$ and $M' \in |\mathbf{Mod}(\Sigma')|$.

$$ M' \models_{\mathcal{INS}, \Sigma'} \mathbf{Sen}(\sigma)(\phi) \iff \mathbf{Mod}(\sigma)(M') \models_{\mathcal{INS}, \Sigma} \phi $$

There are two basic languages within the Event-B language. The first one is the Event-B mathematical language (propositional/predicate logic, set-theory and arithmetic) and the second is the Event-B modelling language [1]. To represent the latter, we propose a new custom solution; for the former, however, we can use $\mathcal{FOPEQ}$, the institution of first-order logic with equality. Thus, our institution for Event-B is built on $\mathcal{FOPEQ}$.

**Definition 2 (FOPEQ-Signature).** A signature in $\mathcal{FOPEQ}$, $\Sigma_{\mathcal{FOPEQ}} = \langle S, \Omega, \Pi \rangle$, is a tuple where $S$ is a set of sort names, $\Omega$ is a set of operation names indexed by arity and sort, and $\Pi$ is a set of predicate names indexed by arity.

**Definition 3 (Σ<sub>FOPEQ</sub>-Sentence).** For any $\Sigma_{\mathcal{FOPEQ}} = \langle S, \Omega, \Pi \rangle$, $\Sigma_{\mathcal{FOPEQ}}$-sentences are closed first-order formulae built out of atomic formulae using $\wedge, \vee, \neg, \Rightarrow, \iff, \exists, \forall$. Atomic formulae are equalities between $\langle S, \Omega \rangle$-terms, predicate formulae of the form $p(t_1, ..., t_n)$ where $p \in \Pi$ and $t_1, ..., t_n$ are terms (with variables), and the logical constants true and false.

**Definition 4 (Σ<sub>FOPEQ</sub>-Model).** Given a signature $\Sigma_{\mathcal{FOPEQ}} = \langle S, \Omega, \Pi \rangle$, a model over $\mathcal{FOPEQ}$ consists of a carrier set $|A|_s$ for each sort name $s \in S$, a
function $f_A : |A|_{s_1} \times \cdots \times |A|_{s_n} \to |A|_s$ for each operation name $f \in \Omega_{s_1 \cdots s_n, s}$ and a relation $p_A \subseteq |A|_{s_1} \times \cdots \times |A|_{s_n}$ for each predicate name $p \in \Pi_{s_1 \cdots s_n}$, where $s_1, \dots, s_n$, and $s$ are sort names.

The satisfaction relation in $\mathcal{FOPEQ}$ is the usual satisfaction of first-order sentences by first-order structures.

## 2.1 Defining $\mathcal{EVT}$

**Definition 5 (EVT-Signature).** A signature in $\mathcal{EVT}$ is a five-tuple $\Sigma_{\mathcal{EVT}} = \langle S, \Omega, \Pi, E, V \rangle$ where $\langle S, \Omega, \Pi \rangle$ is a standard $\mathcal{FOPEQ}$-signature as described above, $E$ is a set of events, i.e. of pairs $\langle \text{event name, status} \rangle$ where status belongs to the poset $\{\text{ordinary} < \text{anticipated} < \text{convergent}\}$, and $V$ is a set of sorted variables. We assume that every signature has an initial event, called `Init`, whose status is always `ordinary`.

*Notation:* We write $\Sigma$ in place of $\Sigma_{\mathcal{EVT}}$ when describing a signature over our institution for Event-B. For signatures over other institutions than $\mathcal{EVT}$ we will use the subscript notation; e.g. a signature over $\mathcal{FOPEQ}$ is denoted by $\Sigma_{\mathcal{FOPEQ}}$. For a given signature $\Sigma$, we access its individual components using a dot-notation, e.g. $\Sigma.V$ for the set $V$ in the tuple $\Sigma$.

**Definition 6 (EVT-Signature Morphism).** A signature morphism $\sigma : \Sigma \to \Sigma'$ is a five-tuple containing $\sigma_S$, $\sigma_\Omega$, $\sigma_\Pi$, $\sigma_E$ and $\sigma_V$. Here $\sigma_S$, $\sigma_\Omega$, $\sigma_\Pi$ are the mappings taken from the corresponding signature morphism in $\mathcal{FOPEQ}$.

- $\sigma_E : \Sigma.E \to \Sigma'.E$ is a function such that for any mapping $\sigma_E \langle e, st \rangle = \langle e', st' \rangle$ we have $st \le st'$; in addition, $\sigma_E$ preserves the initial event: in symbols, we have that $\sigma_E \langle \text{Init}, \text{ordinary} \rangle = \langle \text{Init}, \text{ordinary} \rangle$.

- $\sigma_V : \Sigma.V \to \Sigma'.V$ is a sort-preserving function on sets of variable names, working similarly to the sort-preserving mapping for constant symbols, $\sigma_\Omega$.

**Definition 7 ($\Sigma_{\mathcal{EVT}}$-Sentence).** A sentence over $\mathcal{EVT}$ is a pair $\langle e, \phi(\bar{x}, \bar{x}') \rangle$ where $e$ is an event name in the domain of $\Sigma.E$ and $\phi(\bar{x}, \bar{x}')$ is an open $\mathcal{FOPEQ}$-formula over the variables $\bar{x}$ from $\Sigma.V$ and their primed versions $\bar{x}'$.

In the *Rodin Platform*, Event-B machines are presented (syntactically sug-ared) as can be seen below, where $I(\bar{x})$ represents the invariant over $\bar{x}$.

The variant expression, denoted by $n(\bar{x})$, is used for proving termination properties. Events that have a status of **anticipated** or **convergent** must not increase and strictly decrease the variant expression respectively. Events can have parameter(s) as given by $\bar{p}$. $G(\bar{x}, \bar{p})$ and $W(\bar{x}, \bar{p})$ represent the guard(s) and witness(es) respec-tively over the variables and parameter(s). Actions are interpreted as before-after predi-cates i.e. $x := x + 1$ is interpreted as $x' = x + 1$. Thus, $BA(\bar{x}, \bar{p}, \bar{x}')$ represents the action(s) over

MACHINE m SEES ctx refines a
VARIABLES $\bar{x}$
INVARIANTS $I(\bar{x})$
VARIANT $n(\bar{x})$
EVENTS
Initialisation ordinary
then act-name: BA($\bar{x}, \bar{x}'$)
Event e $\cong$ status
any $\bar{p}$
when guard-name: $G(\bar{x}, \bar{p})$
with witness-name: $W(\bar{x}, \bar{p})$
then act-name: BA($\bar{x}, \bar{p}, \bar{x}'$)

END
the parameter(s) $\bar{p}$ and the sets of variables $\bar{x}$ and $\bar{x}'$.

Sentences written in the mathematical language (such as axioms) are interpreted as sentences over $\mathcal{FOPEQ}$. We can include these in specifications over $\mathcal{EVT}$ using the comorphism which will be defined in Section 3. We represent the Event-B event, variant and invariant sentences as sentences over $\mathcal{EVT}$.

For each Event-B invariant sentence $I(\bar{x})$ we form the open $\mathcal{FOPEQ}$-sentence $I(\bar{x}) \wedge I(\bar{x}')$. Since invariants must hold for all events in a machine, each invariant sentence is paired with each event name $e$ for all $\langle e, s \rangle \in \Sigma.E$, where $s$ is an event status. Thus, we form the $\mathcal{EVT}$ sentence $\langle e, I(\bar{x}) \wedge I(\bar{x}') \rangle$.

The variant expression applies to specific events, so we pair it with an event name in order to meaningfully evaluate it. This expression can be translated into an open $\mathcal{FOPEQ}$-term, which we denote by $n(\bar{x})$, and we use this to construct a formula based on the status of the event(s) in the signature $\Sigma$.

- For each $\langle e, \text{anticipated} \rangle \in \Sigma.E$ we form the sentence $\langle e, n(\bar{x}') \le n(\bar{x}) \rangle$.

- For each $\langle e, \text{convergent} \rangle \in \Sigma.E$ we form the sentence $\langle e, n(\bar{x}') < n(\bar{x}) \rangle$.

Note that we are assuming the existence of a suitable type for variant expressions and the usual arithmetic interpretation of the predicates $<$ and $\le$.

Event guard(s) and witnesses are also labelled predicates that can be translated into open $\mathcal{FOPEQ}$-formulae over the variables $\bar{x}$ in $V$ and parameters $\bar{p}$. These are denoted by $G(\bar{x}, \bar{p})$ and $W(\bar{x}, \bar{p})$ respectively. In Event-B, actions are interpreted as before-after predicates, and so they can be translated into open $\mathcal{FOPEQ}$-formulae denoted by $BA(\bar{x}, \bar{p}, \bar{x}')$. Thus for each event we form the formula $\phi(\bar{x}, \bar{x}') = \exists \bar{p} \cdot G(\bar{x}, \bar{p}) \wedge W(\bar{x}, \bar{p}) \wedge BA(\bar{x}, \bar{p}, \bar{x}')$ where $\bar{p}$ are the event parameters. This generates an $\mathcal{EVT}$-sentence of the form $\langle e, \phi(\bar{x}, \bar{x}') \rangle$. The Init event, which is an Event-B sentence over only the after variables denoted by $\bar{x}'$, is a special case. In this case, we form the $\mathcal{EVT}$-sentence $\langle \text{Init}, \phi(\bar{x}') \rangle$.

There is no formal semantics for Event-B defined in the literature as such. Therefore, we have based our construction of $\mathcal{EVT}$-models on the notion of a mathematical model as described by Abrial [1, Ch. 14]. In these models the state is represented as a sequence of variable-values and models are defined over before and after states. We interpret these states as sets of variable-to-value mappings in our definition of $\mathcal{EVT}$-models.

**Definition 8** ($\Sigma$-State$_A$). For any given $\mathcal{EVT}$-signature $\Sigma$ we define a $\Sigma$-state of an algebra $A$ as a set of (sort appropriate) variable-to-value mappings whose domain is the set of sort-indexed variable names $\Sigma.V$. We define the set State$_A$ as the set of all such $\Sigma$-states. By "sort appropriate" we mean that for any variable $x$ of sort $s$ in $V$, the corresponding value for $x$ should be drawn from $|A|_s$, the carrier set of $s$ given by the $\mathcal{FOPEQ}$-model $A$.

**Definition 9** ($\Sigma_{\mathcal{EVT}}$-Model). Given $\Sigma = \langle S, \Omega, \Pi, E, V \rangle$, $\text{Mod}(\Sigma)$ provides a category of models, where a model over $\Sigma$ is a tuple $\langle A, L, R \rangle$. $A$ is a $\Sigma_{\mathcal{FOPEQ}}$-model, and the non-empty initialising set $L \subseteq \text{State}_A$ provides the states after the Init event. Then for every event name $e \in \text{dom}(E)$, other than Init, we define $R.e \subseteq \text{State}_A \times \text{State}_A$ where for each pair of states $\langle s, s' \rangle$ in R.e, $s$ provides values for the variables $x$ in $V$, and $s'$ provides values for their primed versions $x'$. Then $R = \{R.e \mid e \in \text{dom}(E) \text{ and } e \neq \text{Init}\}$.
Intuitively, a model over $\Sigma$ maps every event name $e \in \text{dom}(\Sigma.E)$ to a set of variable-to-value mappings over the carriers corresponding to the sorts of each of the variables $x \in \Sigma.V$ and their primed versions $x'$. In cases where there are no variables in $\Sigma.V$, $L$ is the singleton $\{\{\}\}$.

For example, given the event $e$ on the right, with natural number variable $x$ and boolean variable $y$ we construct the variable to value mappings:

Event $e \cong$
when $\text{grd1:}$ $x<2$
then $\text{act1:}$ $x := x + 1$
$\text{act2:}$ $y := \text{false}$

$$R_e = \left\{ \begin{array}{l} \{x \mapsto 0, y \mapsto \text{false}, x' \mapsto 1, y' \mapsto \text{false}\}, \quad \{x \mapsto 0, y \mapsto \text{true}, x' \mapsto 1, y' \mapsto \text{false}\}, \\ \{x \mapsto 1, y \mapsto \text{false}, x' \mapsto 2, y' \mapsto \text{false}\}, \quad \{x \mapsto 1, y \mapsto \text{true}, x' \mapsto 2, y' \mapsto \text{false}\} \end{array} \right\}$$

The notation used above is interpreted as *variable name* $\mapsto$ *value* where the value is drawn from the carrier set corresponding to the sort of the variable name given in $\Sigma.V$. We note that trivial models be excluded as the initialising set $L$ is never empty. In cases where there are no variables in $\Sigma.V$, $L$ is the singleton $L = \{\{\}\}$.

The reduct of an $\mathcal{EVT}$-model $M = (A, L, R)$ along an $\mathcal{EVT}$-signature morphism $\sigma : \Sigma \to \Sigma'$ is given by $M|_{\sigma} = (A|_{\sigma}, L|_{\sigma}, R|_{\sigma})$. Here $A|_{\sigma}$ is the reduct of the $\mathcal{FOPEQ}$-component of the $\mathcal{EVT}$-model along the $\mathcal{FOPEQ}$-components of $\sigma$. $L|_{\sigma}$ and $R|_{\sigma}$ are based on the reduction of the states of $A$ along $\sigma$, i.e. for every $\Sigma'$-state $s$ of $A$, that is for every sorted map $s : \Sigma'.V \to |A|$, $s|_{\sigma}$ is the map $\Sigma'.V \to |A|$ given by the composition $\sigma_V; s$. This extends in the usual manner from states to sets of states and to relations on states.

**Satisfaction:** In order to define the satisfaction relation for $\mathcal{EVT}$, we describe an embedding from $\mathcal{EVT}$-signatures and models to $\mathcal{FOPEQ}$-signatures and models.

Given an $\mathcal{EVT}$-signature $\Sigma = (S, \Omega, \Pi, E, V)$ we form the following two $\mathcal{FOPEQ}$-signatures:

- $\Sigma_{\mathcal{FOPEQ}}^{(V, V')} = (S, \Omega \cup V \cup V', \Pi)$ where $V$ and $V'$ are the variables and their primed versions, respectively, that are drawn from the $\mathcal{EVT}$-signature, and represented as 0-ary operators with unchanged sort. The intuition here is that the set of variable-to-value mappings for the free variables in an $\mathcal{EVT}$-signature $\Sigma$ are represented by adding a distinguished 0-ary operation symbol to the corresponding $\mathcal{FOPEQ}$-signature for each of the variables $x \in V$ and their primed versions.

- Similarly, for the initial state and its variables, we construct the signature $\Sigma_{\mathcal{FOPEQ}}^{(V')} = (S, \Omega \cup V', \Pi)$.

Given the $\mathcal{EVT}$-$\Sigma$-model $(A, L, R)$, we construct the $\mathcal{FOPEQ}$-models:

- For every pair of states $(s, s')$, we form the $\Sigma_{\mathcal{FOPEQ}}^{(V, V')}$-model expansion $A^{(s, s')}$, which is the $\mathcal{FOPEQ}$-component $A$ of the $\mathcal{EVT}$-model, with $s$ and $s'$ added as interpretations for the new operators that correspond to the variables from $V$ and $V'$ respectively.

- For each initial state $s' \in L$ we construct the $\Sigma_{\mathcal{FOPEQ}}^{(V')}$-model expansion $A^{(s')}$ analogously.

For any $\mathcal{EVT}$-sentence over $\Sigma$ of the form $\langle e, \phi(\bar{x}, \bar{x}') \rangle$ we create a corresponding $\mathcal{FOPEQ}$-formula by replacing the free variables with their corresponding operator symbols. We write this (closed) formula as $\phi(\bar{x}, \bar{x}')$.
**Definition 10 (Satisfaction Relation).** For any $\mathcal{EVT}$-model $\langle A, L, R \rangle$ and $\mathcal{EVT}$-sentence $\langle e, \phi(\bar{x}, \bar{x}') \rangle$, where $e$ is an event name other than Init, we define:

$$ \langle A, L, R \rangle \models_{\Sigma} \langle e, \phi(\bar{x}, \bar{x}') \rangle \iff \forall \langle s, s' \rangle \in R.e \cdot A^{(s,s')} \models_{\Sigma_{\mathcal{FOPEQ}}^{(V,V')}} \phi(\bar{x}, \bar{x}') $$

Similarly, we evaluate the satisfaction condition of $\mathcal{EVT}$-sentences of the form $\langle \text{Init}, \phi(\bar{x}') \rangle$ as follows:

$$ \langle A, L, R \rangle \models_{\Sigma} \langle \text{Init}, \phi(\bar{x}') \rangle \iff \forall s' \in L \cdot A^{(s')} \models_{\Sigma_{\mathcal{FOPEQ}}^{(V')}} \phi(\bar{x}') $$

**Theorem 1 (Satisfaction Condition).** Given $\mathcal{EVT}$ signatures $\Sigma_1$ and $\Sigma_2$, a signature morphism $\sigma: \Sigma_1 \to \Sigma_2$, a $\Sigma_2$-model $M_2$ and a $\Sigma_1$-sentence $\psi_1$, the following satisfaction condition holds:

$$ \mathbf{Mod}(\sigma)(M_2) \models_{\mathcal{EVT}_{\Sigma_1}} \psi_1 \iff M_2 \models_{\mathcal{EVT}_{\Sigma_2}} \mathbf{Sen}(\sigma)(\psi_1) $$

*Proof.* Let $M_2$ be the model $\langle A_2, L_2, R_2 \rangle$, and $\psi_1$ the sentence $\langle e, \phi(\bar{x}, \bar{x}') \rangle$. Then the satisfaction condition is equivalent to

$$ \begin{align*} \forall \langle s, s' \rangle \in R_2 |_{\sigma} e \cdot (A_2 |_{\sigma})^{(s,s')} |_{\sigma} &\models_{\mathcal{FOPEQ}_{\Sigma_{\mathcal{FOPEQ}}^{(V_1,V'_1)}}} \phi(\bar{x}, \bar{x}') \\ \iff \forall \langle s, s' \rangle \in R_2 \sigma_E(e) \cdot A_2^{(s,s')} &\models_{\mathcal{FOPEQ}_{\Sigma_{\mathcal{FOPEQ}}^{(V_2,V'_2)}}} \mathrm{Sen}(\sigma)(\phi(\bar{x}, \bar{x}')) \end{align*} $$

Here, validity follows from the validity of satisfaction in $\mathcal{FOPEQ}$. We prove a similar result for initial events in the same way. $\square$

**Pragmatics of Specification Building in $\mathcal{EVT}$:** We represent an Event-B specification, such as that for mac1 in Figure 1, as a presentation over $\mathcal{EVT}$. For any signature $\Sigma$, a $\Sigma$-presentation is a set of $\Sigma$-sentences. A model of a $\Sigma$-presentation is a $\Sigma$-model that satisfies all of the sentences in the presentation [5]. Thus, for a presentation in $\mathcal{EVT}$, model components corresponding to an event must satisfy all of the sentences specifying that event. This incorporates the standard semantics of the *extends* operator for events in Event-B where the extending event implicitly has all the parameters, guards and actions of the extended event but can have additional parameters, guards and actions [3].

An interesting aspect is that if a variable is not assigned to within an action, then a model for the event may associate a new value with this variable. Some languages deal with this using a *frame condition*, asserting implicitly that values for unmodified variables do not change. In Event-B such a condition would cause complications when combining presentations, since variables unreferenced in one event will be constrained not to change, and this may contradict an action for them in the other event. As far as we can tell, the informal semantics for the Event-B language do not require a frame condition, and we have not included one in our definition.

## 3 Relating $\mathcal{FOPEQ}$ and $\mathcal{EVT}$

Initially, we defined the relationship between $\mathcal{FOPEQ}$ and $\mathcal{EVT}$ to be a duplex institution formed from a restricted version of $\mathcal{EVT}$ ($\mathcal{EVT}_{res}$) and $\mathcal{FOPEQ}$
where $\mathcal{EVT}_{res}$ is the institution $\mathcal{EVT}$ but does not contain any $\mathcal{FOPEQ}$ components. Duplex institutions are constructed by enriching one institution, in this case $\mathcal{EVT}_{res}$, by the sentences of another, in this case $\mathcal{FOPEQ}$, using an institution semi-morphism [5, 11]. This approach would allow us to constrain $\mathcal{EVT}_{res}$ by $\mathcal{FOPEQ}$ and thus facilitate the use of $\mathcal{FOPEQ}$-sentences in an elegant way. However, duplex institutions are not supported in HETS [9], and therefore we opt for a comorphism which embeds the simpler institution $\mathcal{FOPEQ}$ into the more complex institution $\mathcal{EVT}$ [11].

**Definition 11 (The institution comorphism $\rho$).** We define $\rho: \mathcal{FOPEQ} \to \mathcal{EVT}$ to be an institution comorphism composed of:

- The functor $\rho^{Sign}: \mathbf{Sign}_{\mathcal{FOPEQ}} \to \mathbf{Sign}_{\mathcal{EVT}}$ which takes as input a $\mathcal{FOPEQ}$-signature of the form $\langle S, \Omega, \Pi \rangle$ and extends it with the set $E = \{\langle \text{Init } \text{ordinary} \rangle\}$ and an empty set of variable names $V$. $\rho^{Sign}(\sigma)$ works as $\sigma$ on $S$, $\Omega$ and $\Pi$, it is the identity on the Init event and the empty function on the empty set of variable names.

- The natural transformation $\rho^{Sen}: \mathbf{Sen}_{\mathcal{FOPEQ}} \to \rho^{Sign}; \mathbf{Sen}_{\mathcal{EVT}}$ which pairs any closed $\mathcal{FOPEQ}$-sentence (given by $\phi$) with the Init event name to form the $\mathcal{EVT}$-sentence $\langle \text{Init}, \phi \rangle$. As there are no variables in the signature, we do not require $\phi$ to be over the variables $\bar{x}$ and $\bar{x}'$.

- The natural transformation $\rho^{Mod}: (\rho^{Sign})^{op}; \mathbf{Mod}_{\mathcal{EVT}} \to \mathbf{Mod}_{\mathcal{FOPEQ}}$ is such that for any $\mathcal{FOPEQ}$-signature $\Sigma$,

$$ \rho_{\Sigma}^{\mathrm{Mod}}(\mathrm{Mod}(\rho^{\mathrm{Sign}}(\Sigma))) = \rho_{\Sigma}^{\mathrm{Mod}}(\langle A, L, \emptyset \rangle) = A $$

**Theorem 2.** The institution comorphism $\rho$ is defined such that for any $\Sigma \in |\mathbf{Sign}_{\mathcal{FOPEQ}}|$, the translations $\rho_{\Sigma}^{Sen}: \mathbf{Sen}_{\mathcal{FOPEQ}}(\Sigma) \to \mathbf{Sen}_{\mathcal{EVT}}(\rho^{Sign}(\Sigma))$ and $\rho_{\Sigma}^{Mod}: \mathbf{Mod}_{\mathcal{EVT}}(\rho^{Sign}(\Sigma)) \to \mathbf{Mod}_{\mathcal{FOPEQ}}(\Sigma)$ preserve the satisfaction relation. That is, for any $\psi \in \mathbf{Sen}_{\mathcal{FOPEQ}}(\Sigma)$ and $M' \in |\mathbf{Mod}_{\mathcal{EVT}}(\rho^{Sign}(\Sigma))|$

$$ \rho_{\Sigma}^{\mathrm{Mod}}(M') \models_{\mathcal{FOPEQ}_{\Sigma}} \psi \iff M' \models_{\mathcal{EVT}_{\rho^{Sign}(\Sigma)}} \rho_{\Sigma}^{\mathrm{Sen}}(\psi) \quad (*) $$

*Proof.* By definition 11, $M' = \langle A, L, \emptyset \rangle$, $\rho_{\Sigma}^{Mod}(M') = A$ and $\rho_{\Sigma}^{Sen}(\psi) = \langle \text{Init}, \psi \rangle$. Therefore, we transform (*) into

$$ A \models_{\mathcal{FOPEQ}_{\Sigma}} \psi \iff M' \models_{\mathcal{EVT}_{\rho^{Sign}(\Sigma)}} \langle \text{Init}, \psi \rangle $$

Then, by the definition of satisfaction in $\mathcal{EVT}$ (Definition 10)

$$ A \models_{\mathcal{FOPEQ}_{\Sigma}} \psi \iff A^{(s')} \models_{\mathcal{FOPEQ}_{(\rho^{Sign}(\Sigma))^{(V')}} \psi} $$

We deduce that $\Sigma = (\rho^{Sign}(\Sigma))^{V'}_{\mathcal{FOPEQ}}$, since there are no variable names in $V'$ and thus no new operator symbols are added to the signature. As there are no variable names in $V'$, $L = \{\{\}\}$, so we can conclude that $A^{(s')} = A$. Thus the satisfaction condition holds. $\square$

For a $\Sigma$-specification written over $\mathcal{FOPEQ}$ we can use the specification building operator `-- with $\rho: \mathrm{Spec}_{\mathcal{FOPEQ}}(\Sigma) \to \mathrm{Spec}_{\mathcal{EVT}}(\rho^{Sign}(\Sigma))$` to interpret this as a specification over $\mathcal{EVT}$ [11]. This results in a specification with just the Init event and no variables, containing $\mathcal{FOPEQ}$-sentences that hold in the initial
state. This process is used to represent contexts, specifically their axioms, which are written over $\mathcal{FOPEQ}$ as sentences over $\mathcal{EVT}$.

In cases where a specification is enriched with new events, then the axioms and invariants should also apply to these new events. One approach to this would require a new kind of $\mathcal{EVT}$-sentence for invariants, which we denote by $\langle inv, \phi(\bar{x}, \bar{x}') \rangle$, these are applied to all events in the specification when evaluating the satisfaction condition. We do not present these details fully here due to space concerns.

## 3.1 Pushouts and Amalgamation

We ensure that the institution $\mathcal{EVT}$ has good modularity properties by proving that $\mathcal{EVT}$ admits the amalgamation property: all pushouts in $\mathbf{Sign}_{\mathcal{EVT}}$ exist and every pushout diagram in $\mathbf{Sign}_{\mathcal{EVT}}$ admits weak model amalgamation [11].

**Proposition 1.** *Pushouts exist in $\mathbf{Sign}_{\mathcal{EVT}}$.*

*Proof.* Given two signature morphisms $\sigma_1 : \Sigma \to \Sigma_1$ and $\sigma_2 : \Sigma \to \Sigma_2$ a pushout is a triple $(\Sigma', \sigma'_1, \sigma'_2)$ that satisfies the universal property: for all triples $(\Sigma'', \sigma''_1, \sigma''_2)$ there exists a unique morphism $u : \Sigma' \to \Sigma''$ such that the diagram on the left below commutes. Our pushout construction follows $\mathcal{FOPEQ}$ for the elements that $\mathcal{FOPEQ}$ has in common with $\mathcal{EVT}$. In $\mathbf{Sign}_{\mathcal{EVT}}$ the additional elements are $E$ and $V$.

<figure><img src="image_2.png" /></figure>

- *Set of $\langle event \ name, \ status \rangle$ pairs $E$:* The set of all event names in the pushout is the pushout in **Set** on event names only. Then, the status of an event in the pushout is the supremum of all statuses of all events that are mapped to it. Since signature morphisms map $\langle \mathbf{Init}, \mathbf{ordinary} \rangle$ to $\langle \mathbf{Init}, \mathbf{ordinary} \rangle$ the pushout does likewise. The universality property for $E$ follows from that of **Set**.

- *Set of sort-indexed variable names $V$:* The set of sort-indexed variable names in the pushout is the pushout in $\mathcal{FOPEQ}$ for the sort components and the pushout in **Set** for the variable names. This is a similar construction to the pushout for operation names in $\mathcal{FOPEQ}$ as these also have to follow the sort pushout. Thus, the universality property for $V$ follows from that of **Set** and the $\mathcal{FOPEQ}$ pushout for sorts. $\square$

**Proposition 2.** Every pushout diagram in $\mathbf{Sign}_{\mathcal{EVT}}$ admits weak model amalgamation.

We decompose this proposition into two further subpropositions:

**Proposition 2(a).** For $M_1 \in |\mathbf{Mod}(\Sigma_1)|$ and $M_2 \in |\mathbf{Mod}(\Sigma_2)|$ such that $M_1|_{\sigma_1} = M_2|_{\sigma_2}$, there exists a model (the amalgamation of $M_1$ and $M_2$) $M' \in |\mathbf{Mod}(\Sigma')|$ such that $M'|_{\sigma'_1} = M_1$ and $M'|_{\sigma'_2} = M_2$.
<figure><img src="image_3.png" /><figcaption>Fig. 4: A modular institution-based presentation corresponding to the abstract machine mac1 in Fig 1.</figcaption></figure>

We get a presentation over the institution $\mathcal{EVT}$ for mac1 by flattening out the structuring. Notice that the specification for each individual light had to be explicitly written down twice in the Event-B machine in Figure 1 (lines 11–15 and lines 16–20). In our modular institution-based presentation we only need one light specification and simply supply the required variable and event mappings. In this way, $\mathcal{EVT}$ provides a more flexible degree of modularity than is currently present in Event-B.

## 4.1 Refinement in the $\mathcal{EVT}$ Institution

Event-B supports three forms of machine refinement: the refinement of event internals (guards and actions) and invariants; the addition of new events; and the decomposition of an event into several events [2]. It is therefore essential for any formalisation of Event-B to be capable of capturing refinement.

In general for institutions, a refinement from an abstract specification A to some concrete specification C is defined using model-class inclusion as $|\text{Mod}(C)| \subseteq |\text{Mod}(A)|$ when $\text{Sig}[A] = \text{Sig}[C]$. In Event-B, new variable or event names cannot be added if the signatures stay the same. This provides only one option: strengthen the formulae in event definitions, which will result in at most the same number of models. This accounts for the first form of refinement in Event-B. Both of the other forms of refinement in Event-B cause the signatures to change i.e. the set of events will get larger when adding or decomposing events. In the case when the signatures are different, we can define a signature morphism $\sigma: \text{Sig}[A] \to \text{Sig}[C]$ from which we can construct the model reduct $\text{Mod}(\sigma): \text{Mod}(C) \to \text{Mod}(A)$. We can thus restrict the concrete model to only contain elements of the abstract signatures by applying the model reduct before evaluating the subset relation defined above.

## 4.2 A Modular, Refined Specification

Figure 5 contains a presentation over $\mathcal{EVT}$ corresponding to the main elements of the Event-B specification MAC2 presented in Figures 2 and 3. Here, we present three CASL specifications and three $\mathcal{EVT}$ specifications.
<figure><img src="image_4.png" /><figcaption>Fig. 5: A modular institution-based presentation corresponding to the refined machine `mac2` specified in Fig 3.</figcaption></figure>

**Lines 1–10:** We specify the *Colours* data type with a standard *CASL* specification, as can be seen in Figure 2. The specification *TWOCOLOURS* describes two variables of type *Colours* constrained to be not both green at the same time. This corresponds to the gluing invariants on lines 5 and 7 of Figure 3. The specification modularisation constructs used in Figure 5, allow these properties to be handled distinctly and in a manner that facilitates comparison with the *TWOBOOLS* specification on lines 1–6 of Figure 4.

**Lines 15–25:** A specification for a single light is provided in *LIGHTREFINED* which uses *TWOCOLOURS* to describe the colour of the lights. As was the case with *LIGHTABSTRACT* in Figure 4, the specification makes clear how a single light operates. An added benefit here is that a direct comparison with the abstract specification can be done on a per-light basis.

**Lines 11–14, 26–34:** The specifications `BOOLBUTTON` and `BUTTONSPEC` account for the part of the `MAC2` specification that requires a button. These details were woven through the code in Figure 3 (lines 2, 8, 16, 18, 29, 30) but the specification-building operators allow us to modularise the specification and group these related definitions together, clarifying how the button actually operates.

**Lines 35–51:** Finally, to bring this all together we combine a copy of *LIGHTREFINED* with a specification corresponding to the sum (and) of *LIGHTREFINED* and `BUTTONSPEC` with appropriate signature morphisms. This second specification combines the event `gobutton` in `BUTTONSPEC` with the event `set.green` in *LIGHTREFINED* thus accounting for `set.peds.green` in Figure 3. One small
<figure><img src="image_5.png" /><figcaption>Fig. 6: Defining the refinement relationships between the concrete and abstract presentations.</figcaption></figure>

issue involves making sure that the name replacements are done correctly, and in the correct order, hence the bracketing on lines 37–38 is important.

The combination of these specifications involves merging two events with different names: `gobutton` from `BUTTONSPEC` with the event `set-green` from `LIGHTREFINED`. To ensure that these differently-named events are combined into an event of the same name we use the signature morphism $\sigma_5$ to give `gobutton` the same name as `set-green` before combining them. Ensuring that the events have the same name allows the `and` operator to combine both events’ guards and actions and the morphism $\sigma_4$ to name the resulting event `set-peds-green`. The resulting specification also contains the event `pushbutton`. The labels given to guards/actions are syntactic sugar to make the specification aesthetically resemble the usual Event-B notation for guards/actions.

Figure 6 uses the refinement syntax available in HETS to specify each of the refinements in the specification of the concrete machine `mac2`:

**Lines 2–4:** define the data refinement of `Bool` into `Colours`, with an appropriate mapping for the values.

**Lines 5–6:** define the refinement of the two boolean variables into their corresponding variables of type `Colour`. In combination with lines 2–4, this corresponds to the gluing invariants on lines 5 and 7 of Figure 3.

**Lines 7–14:** define the refinement relation between the four events: this corresponds to the `refines` statements on lines 14, 20, 23 and 27 of Figure 3.

# 5 Conclusion and Future Work

Currently, the core benefit of $\mathcal{EVT}$, our institution for Event-B, is the increased modularity of Event-B specifications via the use of specification-building operators. The concept of refinement, central to Event-B, is also well-developed in the theory of institutions, and we have shown how this can be applied here. Devising meaningful institutions and corresponding morphisms to/from Event-B provides a mechanism not only for ensuring the safety of a particular specification but also, via morphisms, a potential for integration with other formalisms. Interoperability and heterogeneity are significant goals in the field of software engineering, and we believe that the work presented in this paper provides a basis for the integration of Event-B with other formalisms defined in this way.

The Heterogeneous Tool-Set HETS provides a framework for heterogeneous specifications where each formalism is represented as a logic and understood in the theory of institutions [9]. Our logic for $\mathcal{EVT}$ utilises the already existing
institution CASL [10] to account for the FOPEQ parts of the EVT institution
thus taking advantage of the interoperability/heterogeneity supplied by HETS.
CASL provides sorts and predicates like those written in lines 4–6 from Figure 4.

At present we can parse, statically analyse and combine specifications written over *EVT*. Future work includes developing comorphisms to translate between *EVT* and other logics in HETS as well as integrating with the provers currently available in HETS (e.g. Isabelle). Comorphisms between these theorem provers and *EVT* will allow us to prove our specifications correct in HETS. We envisage that development should take place here to fully take advantage of the prospects for interoperability. A translation from Event-B to *EVT* in the future will not only enable us to fully utilise both the *Rodin Platform* and HETS, but will also provide a translational semantics for Event-B using the theory of institutions.

**Acknowledgements** The authors would like to acknowledge the reviewers for their helpful comments and Ionut Tutu for his assistance with the presentation of the technical details of our institution for Event-B.

References

1. J.-R. Abrial. *Modeling in Event-B: System and Software Engineering*. Cambridge University Press, New York, NY, USA, 1st edition, 2010.

2. J.-R. Abrial, M. Butler, S. Hallerstede, T. S. Hoang, F. Mehta, and L. Voisin. Rodin: an open toolset for modelling and reasoning in Event-B. *International Journal on Software Tools for Technology Transfer*, 12(6):447–466, 2010.

3. J.-R. Abrial and S. Hallerstede. Refinement, decomposition, and instantiation of discrete models: Application to Event-B. *Fundamenta Informaticae*, 77(1-2):1–28, 2007.

4. A. Achouri and L. Jemni Ben Ayed. UML activity diagram to Event-B: A model transformation approach based on the institution theory. In *Information Reuse and Integration*, pages 823–829, Aug. 2014.

5. J. A. Goguen and R. M. Burstall. Institutions: abstract model theory for specification and programming. *Journal of the ACM*, 39(1):95–146, 1992.

6. A. Iliasov, E. Troubitsyna, L. Laibinis, A. Romanovsky, K. Varpaaniemi, D. Ilic, and T. Latvala. Supporting reuse in Event-B development: Modularisation approach. In *Abstract State Machines, Alloy, B and Z*, volume 5977 of LNCS, pages 174–188, 2010.

7. M. Jastram and P. M. Butler. *Rodin User's Handbook: Covers Rodin V.2.8*. CreateSpace Independent Publishing Platform, USA, 2014.

8. A. Knapp, T. Mossakowski, M. Roggenbach, and M. Glauer. An institution for simple UML state machines. In *Fundamental Approaches to Software Engineering*, volume 9033 of LNCS, pages 3–18, 2015.

9. T. Mossakowski, C. Maeder, and K. Lüttich. The heterogeneous tool set, HETS. In *Tools and Algorithms for the Construction and Analysis of Systems*, volume 4424 of LNCS, pages 519–522, 2007.

10. P. D. Mosses, editor. *CASL Reference Manual*, volume 2960 of LNCS. Springer, 2004.

11. D. Sanella and A. Tarlecki. *Foundations of Algebraic Specification and Formal Software Development*. Springer, 2012.