Farrell, Marie and Monahan, Rosemary and Power, James F. (2023) Building Specifications in the Event-B Institution: A Summary. Rigorous State-Based Methods, 14010. pp. 245-253. ISSN 0302-9743

Download (705kB)

Abstract

This “journal-first” paper summarises a publication by the same authors in the journal Logical Methods in Computer Science which describes a formal semantics for the Event-B specification language using the theory of institutions. It defines an institution for Event-B and shows how the constructs of the Event-B specification language can be mapped into our institution. This algebraic semantics distinguishes three constituent sub-languages of Event-B: the superstructure, infrastructure and mathematical languages. An important impact of this work is that our semantics provides access to the generic modularisation constructs available in institutions, including specification-building operators for parameterisation and refinement. We demonstrate how these features subsume and enhance the corresponding features already present in Event-B through a detailed study of their use in a worked example. Further benefits of the institutional approach are its provision for mathematically definable interoperability to facilitate heterogeneous specification.

Item Type:	Article
Keywords:	Event-B; Semantics; Modularisation; Interoperability;
Academic Unit:	Faculty of Science and Engineering > Computer Science
Item ID:	18574
Identification Number:	https://doi.org/10.1007/978-3-031-33163-3_19
Depositing User:	Marie Farrell
Date Deposited:	23 May 2024 11:43
Journal or Publication Title:	Rigorous State-Based Methods
Publisher:	springer link
Refereed:	Yes
URI:	Publisher
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