# An Institution for Event-B

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 $\mathcal {EVT}$. We provide a definition of $\mathcal {EVT}$ and the proof of its satisfaction condition. A motivating example of a traffic-light simulation is presented to illustrate our approach.
Keywords :
Document type :
Conference papers
Domain :

Cited literature [10 references]

https://hal.inria.fr/hal-01767469
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Monday, April 16, 2018 - 11:34:53 AM
Last modification on : Thursday, May 27, 2021 - 12:50:01 PM

### File

433330_1_En_8_Chapter.pdf
Files produced by the author(s)

### Citation

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⟩

Record views