An institution for event-B

M. Farrell, R. Monahan, J.F. Power

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review


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.
Original languageEnglish
Title of host publicationInternational Workshop on Algebraic Development Techniques
Subtitle of host publicationWADT 2016: Recent Trends in Algebraic Development Techniques
Number of pages16
Publication statusPublished - 8 Dec 2017


Dive into the research topics of 'An institution for event-B'. Together they form a unique fingerprint.

Cite this