«Abstract. This paper presents a formulation of the Event-B formal speciﬁcation language in terms of the theory of institutions. Our goal is to ...»
An Institutional Approach to
Modularisation in Event-B
Marie Farrell, Rosemary Monahan, and James F. Power
Dept. of Computer Science, Maynooth University, Co. Kildare, Ireland
Abstract. This paper presents a formulation of the Event-B formal
speciﬁcation language in terms of the theory of institutions. Our goal is
to exploit the speciﬁcation-building operations of this theory to modu-
larise Event-B speciﬁcations. A case study of a traﬃc-light simulation is
presented to illustrate our approach.
Keywords: Event-B; institutions; reﬁnement; formal methods; modular speciﬁcation 1 Introduction and Motivation Event-B is a state-based formalism for system-level modelling and veriﬁcation, combining set theoretic notation with event-driven modelling. Event-B ensures the safety of a given speciﬁcation via proof-obligation generation and theorem proving with support for these provided by the Rodin Platform [5, 8].
The main pitfalls of Event-B are that it lacks well-developed modularisation constructs and it is not easy to combine speciﬁcations in Event-B with those written in other formalisms . Our thesis, presented in this paper, is that the theory of institutions can provide a framework for deﬁning a rich set of modulari- sation operations and promoting interoperability and heterogeneity for Event-B.
Examples of formalisms that have been improved by using institutions in this way are those for UML state machines  and CSP .
This paper is centered around a case study of a speciﬁcation in Event-B, inspired by one in the Rodin Handbook , and we use this to give an overview of Event-B and related work in Section 2. To use the speciﬁcation-building oper- ators provided by institutions we deﬁne an institution for Event-B in Section 3.
This allows us to re-cast our case study in modular form. We address reﬁnement in Section 4 since this is of central importance in Event-B, and show how this too can be modularised using institutional speciﬁcation building operations. We summarise our contributions and outline future directions in Section 5.
2 Event-B Event-B machines are used for modelling the dynamic part of a systems spec- iﬁcation . Figure 1 presents an Event-B machine for a traﬃc lights system This project is funded by the Irish Research Council, email: firstname.lastname@example.org with one light signalling cars and one signalling pedestrians . The goal of the speciﬁcation 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 ﬂags on line 3).
In general, machine speciﬁcations can contain variable declarations (lines 2-3), invariants (lines 4-7) and event speciﬁcations (lines 8-33).
Figure 1 speciﬁes ﬁve kinds of event (including a starting event called Init- ialisation (lines9-13)). Each event speciﬁcation has a guard part, specifying when it can be activated, and an action part, specifying what happens when the event is activated. For example, the set peds go event as speciﬁed on lines 14-19, has one guard expressed as a boolean expression (line 16), and one action, expressed as an assignment statement (line 18). In general an event can contain many guards and actions, though a variable can only be assigned to once (and assignments occur in parallel).
In addition to machine speciﬁcations, contexts in Event-B can be used model the static properties of a system (constants, axioms and carrier sets). Figure 2 provides a context giving a speciﬁcation for the data-type COLOU RS and uses the axiom on line 7 to explicitly restrict the set to only contain the constants red, green and orange.
A central feature of Event-B is its support for reﬁnement, allowing a developer to write an
speciﬁcation of a system and gradually add complexity through a series of reﬁnement steps [3, 11]. Figure 3 shows an Event-B machine speciﬁcation for mac2 which reﬁnes the machine mac1 from Figure 1. This machine is reﬁned ﬁrst by introducing the new context on line 3 and then by replacing the truth values used in the abstract machine with new values from the carrier set COLOU RS. During reﬁnement, the user typically supplies a gluing invariant relating properties of the abstract machine to their counterparts in the concrete machine . The gluing invariants shown in lines 8 and 10 of Figure 3 deﬁne a one-to-one mapping between the concrete variables introduced in mac2 and the abstract variables of mac1. As speciﬁed in lines 7 and 9, the new variables (peds colour and cars colour) can be either red or green, thus the gluing invariants map true to green and f alse to red.
Event-B permits the addition of new variables and events - buttonpushed on line 5 and press button on lines 44-46. Also, the existing events from mac1 are renamed to reﬂect reﬁnement; for example, on lines 18-19 the event set pedsgreen is declared to reﬁne set peds go. This event has also been altered via the addition of a guard (line 22) and an action (line 25) which incorporate the functionality of a button-controlled pedestrian light.
This example highlights features of the Event-B language, but notice how, in Figure 1 the same speciﬁcation has to be provided twice. 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 speciﬁcation for these events should only happen once. Also, the invariants in Figure 1 (lines 6,7,8) are concerned with typing. It is superﬂuous to check typing as often as invariant preservation. In an ideal world, these fundamental details would be dealt with elsewhere.
The Event-B formalism lacks modularisation constructs which will improve its scalability for use in industrial projects . One suggested method of providing modularity for Event-B speciﬁcations is model decomposition, originally proposed by Abrial and later developed as a plugin for the Rodin Platform [3, 17].
Two methods of model decomposition were addressed by Abrial: shared variable and shared event. Shared variable partitions the model into subcomponents based on events sharing the same variables. The shared event method partitions the model based on variables participating in the same events. An event that uses variables from diﬀerent subcomponents must be split into partial versions of the non-decomposed event (restricted to only parameters, guards and actions referring to the relevant variable). To use the plugin the user selects the machine to be decomposed and deﬁnes the subcomponents to be generated. They then select the style of decomposition to use and can opt to decompose the contexts in a similar fashion. The tool generates the subcomponents which can undergo further reﬁnement and be recomposed . The moment in development where decomposition takes place is important: decomposing early may yield an overly abstract sub-component that cannot be reﬁned without knowledge of the others; decomposing late may mean that the already concrete model will not beneﬁt from the decomposition. In addition, this approach is quite restrictive in that it is not possible to refer to the same element across subcomponents. Also, it is impossible to select which invariants are allocated to each subcomponent, currently, only those relating to variables of the subcomponent are included.
Another approach is the modularisation plugin for Rodin , which is based on the shared variable method outlined above. Here, modules split up an Event-B component and are paired with an interface describing conditions for incorporating the module into another. Module interfaces list the operations contained in the module. These are similar to machines but they may not specify events.
The events of a machine which imports an interface can see the visible constants, sets and axioms, call the imported operations, and the interface variables and invariants are added to the machine. These imported interface variables may be referred to in invariants/guards and actions but may not be directly updated in an action.
Although similar to the shared variable approach proposed by  this method is less restrictive, as invariants can be included in the module interface. This provides a mechanism for modularity in Event-B but there are a large number of diﬀerent components that the user needs to utilise and it is unclear how a model developed using these constructs might be translated into/combined with a diﬀerent formalism. It does not improve the overall scalability of Event-B as a formalism but rather increases modularity within Event-B only .
By providing an institution for the Event-B formalism, we increase the the modularity of Event-B speciﬁcations via the use of speciﬁcation building operators . Furthermore, our approach provides scope for the interoperability of Event-B and other formalisms. The development of EVT, our institution for Event-B, has been closely based on UML, the institution for UML state machines . Both institutions describe state-based formalisms and, therefore, by keeping UML in mind during the development of EVT, it should be possible to design meaningful signature morphisms between these formalisms in the future.
UML-B (Rodin plugin) provides a way of moving from UML models to Event-B code, but this was not developed with institutions in mind . Our Hets implementation of EVT takes inspiration from that of CSPCASL in Hets which uses CASL to specify the data parts of CSP processes . This will become clearer when we discuss separating out Event-B speciﬁcations in Section 3.
An attempt has already been made to provide an institution and corresponding morphisms for Event-B and UML . However, the deﬁnition of Event-B sentences and models are vague, making it diﬃcult to evaluate their semantics in a meaningful way. Also, the models described more closely resemble the settheoretic foundations of B speciﬁcations, whereas we concentrate on event-based models in EVT. While it is always possible to describe formalisms to some extent using institutions, the presentation of a case study in both Event-B and its modular, institutional version is an important element of developing this work.
An institution exists for CSP in which models are described as traces .
The main issue in developing meaningful morphisms between EVT and CSP arises from the fact that CSP is a much richer language than Event-B (and thus EVT ). This means that although it appears easy to move from EVT to CSP, the opposite direction will be more diﬃcult. That said, the work of Schneider et al. provides a basis for such a translation by contributing a CSP semantics of Event-B .
Other related work includes various plugins that translate between diﬀerent formalisms and Event-B; however thus far none use institution theory to do so.
The theory of institutions, originally developed by Goguen and Burstall in a series of papers originating from their work on algebraic speciﬁcation, was ultimately generalised to include multiple formalisms . The key observation is that once the syntax and semantics of a formal system have been deﬁned in a uniform way, using some basic constructs from category theory, then a set of speciﬁcation building operators can be deﬁned that allow you to write, modularise and build up speciﬁcations that can be deﬁned in a formalism-independent manner .
Institutions have been deﬁned for many logics and formalisms, most notably algebraic speciﬁcation and variants of ﬁrst-order logic, but also programmingrelated formal languages relevant to Event-B such as UML state machines , CSP  and Z speciﬁcations .
Deﬁnition(Institution) Formally, an institution IN S for some given formalism will consist of deﬁnitions for Vocabulary: a category Sign of signatures, with signature morphisms σ : Σ → Σ for each signature Σ, Σ ∈ |Sign|.
5 Syntax: a functor Sen : Sign → Set giving a set Sen(Σ) of Σ-sentences for each signature Σ and a function Sen(σ) : Sen(Σ) → Sen(Σ ) which translates Σ-sentences to Σ -sentences for each signature morphism σ.
Semantics: a functor Mod : Signop → Cat giving a category Mod(Σ) of Σ-models for each signature Σ and a functor Mod(σ) : Mod(Σ ) → Mod(Σ) which translates Σ -models to Σ-models (and Σ -morphisms to Σ-morphisms) for each signature morphism σ : Σ → Σ.
Satisfaction: a satisfaction relation |=IN S,Σ ⊆ |Mod(Σ)| × Sen(Σ), determining satisfaction of Σ-sentences by Σ-models for each signature Σ, such that for any signature morphism σ the translations Mod(σ) of models and Sen(σ)
of sentences preserve the satisfaction relation:
for any φ ∈ Sen(Σ) and M ∈ |Mod(Σ )| .
Deﬁning EVT, an institution for Event-B 3.1 EVT, our formalisation of Event-B in terms of institutions is based on splitting
an Event-B speciﬁcation into two parts:
– A data part, which can be deﬁned using some standard institution such as that for algebra or ﬁrst-order logic. We have chosen FOPEQ, the institution for ﬁrst order predicate logic with equality , since it most closely matches the kind of data speciﬁcation needed.
– An event part, which deﬁnes a set of events in terms of formula constraining their before- and after- states. Our speciﬁcation here is closely based on UML, an institution for UML state machines .
While we do not have space to present the details fully formally here, they are not more complex than those normally used for ﬁrst-order logic, with appropriate assignments for the free variables named in the event speciﬁcation variables.
A signature in EVT is a tuple Σ, where Σ = S, Ω, Π, E, V with S, Ω, Π a standard ﬁrst-order signature consisting of a set of sort, operation and predicate names, the latter two indexed appropriately by sort and arity. E is a set of event names which must contain the event name Initialisation. V is a set of sortindexed variable names. Signature morphisms respect arities, sort-indexing and initialisation events.
For any Σ = S, Ω, Π in FOPEQ, a Σ-sentence is a set of closed ﬁrst-order formulae built out of atomic formulae using (∧, ∨, ¬, ⇒, ⇐⇒, ∃, ∀). Formulae are algebraic term equalities ( S, Ω -terms) over the predicates, variables and, true and false.