Farrell, Marie and Monahan, Rosemary and Power, James F. (2017) An Institution for Event-B. In: Recent Trends in Algebraic Development Techniques : Revised Selected Papers. Lecture Notes in Computer Science (10644). Springer, Cham, Switzerland, pp. 104-119. ISBN 978-3-319-72043-2

Preview

Download (1MB) | Preview

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.

Item Type:	Book Section
Additional Information:	This paper was presented at the 23rd IFIP WG 1.3 International Workshop, WADT 2016, Gregynog, UK, September 21–24, 2016.
Keywords:	Event-B; Institutions; Refinement; Formal methods; Modular specification; Formal specification;
Academic Unit:	Faculty of Science and Engineering > Computer Science Faculty of Science and Engineering > Research Institutes > Hamilton Institute
Item ID:	12011
Identification Number:	https://doi.org/10.1007/978-3-319-72044-9_8
Depositing User:	Rosemary Monahan
Date Deposited:	06 Dec 2019 12:15
Publisher:	Springer
Refereed:	Yes
URI:	Publisher Organisation
Use Licence:	This item is available under a Creative Commons Attribution Non Commercial Share Alike Licence (CC BY-NC-SA). Details of this licence are available here

Repository Staff Only(login required)

Item control page

Downloads

Origin of downloads