FREE ELECTRONIC LIBRARY - Dissertations, online materials

Pages:   || 2 | 3 |

«Abstract. This paper presents a formulation of the Event-B formal specification language in terms of the theory of institutions. Our goal is to ...»

-- [ Page 1 ] --

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

specification language in terms of the theory of institutions. Our goal is

to exploit the specification-building operations of this theory to modu-

larise Event-B specifications. A case study of a traffic-light simulation is

presented to illustrate our approach.

Keywords: Event-B; institutions; refinement; formal methods; modular specification 1 Introduction and Motivation Event-B is a state-based formalism for system-level modelling and verification, combining set theoretic notation with event-driven modelling. Event-B ensures the safety of a given specification 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 specifications in Event-B with those written in other formalisms [7]. Our thesis, presented in this paper, is that the theory of institutions can provide a framework for defining 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 [9] and CSP [13].

This paper is centered around a case study of a specification in Event-B, inspired by one in the Rodin Handbook [8], and we use this to give an overview of Event-B and related work in Section 2. To use the specification-building oper- ators provided by institutions we define an institution for Event-B in Section 3.

This allows us to re-cast our case study in modular form. We address refinement in Section 4 since this is of central importance in Event-B, and show how this too can be modularised using institutional specification 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- ification [2]. Figure 1 presents an Event-B machine for a traffic lights system This project is funded by the Irish Research Council, email: mfarrell@cs.nuim.ie with one light signalling cars and one signalling pedestrians [8]. The goal of the specification 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 3).

In general, machine specifications can contain variable declarations (lines 2-3), invariants (lines 4-7) and event specifications (lines 8-33).

Figure 1 specifies five kinds of event (including a starting event called Init- ialisation (lines9-13)). Each event specification 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 specified 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 specifications, 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 specification 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 refinement, allowing a developer to write an


specification of a system and gradually add complexity through a series of refinement steps [3, 11]. Figure 3 shows an Event-B machine specification for mac2 which refines the machine mac1 from Figure 1. This machine is refined first 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 refinement, the user typically supplies a gluing invariant relating properties of the abstract machine to their counterparts in the concrete machine [8]. The gluing invariants shown in lines 8 and 10 of Figure 3 define a one-to-one mapping between the concrete variables introduced in mac2 and the abstract variables of mac1. As specified 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 reflect refinement; for example, on lines 18-19 the event set pedsgreen is declared to refine 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 specification 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 specification for these events should only happen once. Also, the invariants in Figure 1 (lines 6,7,8) are concerned with typing. It is superfluous 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 [7]. One suggested method of providing modularity for Event-B specifications 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 different 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 defines 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 refinement and be recomposed [17]. The moment in development where decomposition takes place is important: decomposing early may yield an overly abstract sub-component that cannot be refined without knowledge of the others; decomposing late may mean that the already concrete model will not benefit 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 [7], 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 [3] 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 different 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 different formalism. It does not improve the overall scalability of Event-B as a formalism but rather increases modularity within Event-B only [7].

By providing an institution for the Event-B formalism, we increase the the modularity of Event-B specifications via the use of specification building operators [14]. 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 [9]. 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 [18]. Our Hets implementation of EVT takes inspiration from that of CSPCASL in Hets which uses CASL to specify the data parts of CSP processes [12]. This will become clearer when we discuss separating out Event-B specifications in Section 3.

An attempt has already been made to provide an institution and corresponding morphisms for Event-B and UML [4]. However, the definition of Event-B sentences and models are vague, making it difficult to evaluate their semantics in a meaningful way. Also, the models described more closely resemble the settheoretic foundations of B specifications, 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 [13].

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 difficult. That said, the work of Schneider et al. provides a basis for such a translation by contributing a CSP semantics of Event-B [15].

Other related work includes various plugins that translate between different formalisms and Event-B; however thus far none use institution theory to do so.

3 Institutions

The theory of institutions, originally developed by Goguen and Burstall in a series of papers originating from their work on algebraic specification, was ultimately generalised to include multiple formalisms [6]. The key observation is that once the syntax and semantics of a formal system have been defined in a uniform way, using some basic constructs from category theory, then a set of specification building operators can be defined that allow you to write, modularise and build up specifications that can be defined in a formalism-independent manner [14].

Institutions have been defined for many logics and formalisms, most notably algebraic specification and variants of first-order logic, but also programmingrelated formal languages relevant to Event-B such as UML state machines [9], CSP [13] and Z specifications [10].

Definition(Institution) Formally, an institution IN S for some given formalism will consist of definitions 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(Σ )| [14].

Defining 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 specification into two parts:

– A data part, which can be defined using some standard institution such as that for algebra or first-order logic. We have chosen FOPEQ, the institution for first order predicate logic with equality [14], since it most closely matches the kind of data specification needed.

– An event part, which defines a set of events in terms of formula constraining their before- and after- states. Our specification here is closely based on UML, an institution for UML state machines [9].

While we do not have space to present the details fully formally here, they are not more complex than those normally used for first-order logic, with appropriate assignments for the free variables named in the event specification variables.

A signature in EVT is a tuple Σ, where Σ = S, Ω, Π, E, V with S, Ω, Π a standard first-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 first-order formulae built out of atomic formulae using (∧, ∨, ¬, ⇒, ⇐⇒, ∃, ∀). Formulae are algebraic term equalities ( S, Ω -terms) over the predicates, variables and, true and false.

Pages:   || 2 | 3 |

Similar works:

«Shoji Makino Te-Won Lee Hiroshi Sawada Blind Speech Separation SPIN Springer’s internal project number, if known Springer Berlin Heidelberg New York Barcelona Budapest Hong Kong London Milan Paris Santa Clara Singapore Tokyo Contents 14 Sparsification for Monaural Source Separation........... 1 Hiroki Asari, Rasmus K. Olsson, Barak A. Pearlmutter, Anthony M. Zador 14.1 Introduction................................................. 1...»

«The Thrill and the Thrall of the Thing By Anne Wordsworth January 26, 2014 A Major Paper submitted to the Faculty of Environmental Studies in partial fulfillment of the requirements for the degree of Master in Environmental Studies. York University, Toronto, Ontario, Canada _ _ Anne Wordsworth Catriona Sandilands MES Candidate Major Paper Supervisor Abstract It is necessary to restrain our consumption practices if we are to have any hope of reversing the escalating environmental damage being...»

«NOTICE: This opinion is subject to motions for rehearing under Rule 22 as well as formal revision before publication in the New Hampshire Reports. Readers are requested to notify the Reporter, Supreme Court of New Hampshire, One Charles Doe Drive, Concord, New Hampshire 03301, of any editorial errors in order that corrections may be made before the opinion goes to press. Errors may be reported by E-mail at the following address: reporter@courts.state.nh.us. Opinions are available on the...»


«A STUDY OF POVERTY AND PROSPERITY IN THE BOOK OF PROVERBS A Thesis Presented to the Faculty of the Department of Semitics and Old Testament Studies Dallas Theological Seminary In Partial Fulfillment of the Requirements for the Degree Master of Theology by C. Frederick Tempies August 1980 TABLE OF CONTENTS Chapter I. INTRODUCTION 1 Need for the Study Purpose of the Study Procedure of the Study II. THE DEFINITION OF POVERTY AND PROSPERITY 6 Terms for poverty Terms for prosperity Synonyms for...»

«Leabharlann Náisiúnta na hÉireann National Library of Ireland Collection List No. 129 Lismore Castle Papers [MSS 6315-7220, 12,813, 13,226-13,256, 22,068, 41,981-41,985, 43,087-43,121, 43,140-43,226, 43,266-43,310, 43,346-43,553, 43,580-43,732, 43,733-43,815, 43,88944,018, MS Maps 366-491, and Arch. Drawings AD 3594/ 1-13] (Accession 1188) The Lismore Castle papers are a very large and important collection of the records of the estates of the Boyle family, Earls of Cork and Burlington and...»

«इंटरनेट मानक Disclosure to Promote the Right To Information Whereas the Parliament of India has set out to provide a practical regime of right to information for citizens to secure access to information under the control of public authorities, in order to promote transparency and accountability in the working of every public authority, and whereas the attached publication of the Bureau of Indian Standards is of particular interest to the public, particularly disadvantaged...»


«Vegard Huse Analysis and design of the SEVAN FPSO against abnormal ice actions Master’s Thesis Supervisor Professor Jørgen Amdahl Trondheim, June 2010 Norwegian University of Science and Technology Department of Marine Technology MASTER THESIS SPRING 2010 for Stud. Techn. Vegard Huse Analysis and design of the SEVAN FPSO against abnormal ice actions Analyse og dimensjonering SEVAN FPSO mot ekstreme islaster As the exploration and exploitation for hydrocarbons move to arctic waters severe ice...»

«Vaccines 2014, 2, 422-462; doi:10.3390/vaccines2020422 OPEN ACCESS vaccines ISSN 2076-393X www.mdpi.com/journal/vaccines Review Therapeutic Vaccine Strategies against Human Papillomavirus Hadeel Khallouf, Agnieszka K. Grabowska and Angelika B. Riemer * Immunotherapy and -prevention, German Cancer Research Center (DKFZ), Heidelberg 69120, Germany; E-Mails: h.khallouf@dkfz.de (H.K.); a.grabowska@dkfz.de (A.K.G.) * Author to whom correspondence should be addressed; E-Mail: a.riemer@dkfz.de; Tel.:...»

«MANUAL DE PROCEDIMIENTOS PARA EL OTORGAMIENTO DE PATENTES C.I.P.A. El presente manual cumple el propósito de informar y orientar al contribuyente, en los trámites de solicitud de una patente comercial para las distintas actividades o giros comerciales que se realizan.¿COMO OBTENGO MI PATENTE COMERCIAL? Es importante que el Contribuyente comprenda que antes de arrendar, comprar o invertir en un local para realizar una actividad comercial, se informe en primer lugar, acerca del Plano Regulador...»

«1 ARTISAN FOOD INNOVATION VOUCHERS Frequently Asked Questions _ Q1: Who is eligible to apply? Q2: How does the Artisan Food Innovation Voucher Programme work? Q3: How can I apply? Q4: When can I apply? Q5: Do I have to be a client of Enterprise Ireland to apply? Q6: How many vouchers will be awarded? Q7: I am a sole trader, can I apply for an artisan food innovation voucher? Q8: What is an Approval/Registration Number? Q9: What do we do if we receive a voucher? Q10: Are vouchers subject to VAT?...»

<<  HOME   |    CONTACTS
2016 www.dissertation.xlibx.info - Dissertations, online materials

Materials of this site are available for review, all rights belong to their respective owners.
If you do not agree with the fact that your material is placed on this site, please, email us, we will within 1-2 business days delete him.