Farrell, Marie, 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
Preview
Available under License Creative Commons Attribution Non-commercial Share Alike.
Download (705kB) | Preview
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: | 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 |
| Related URLs: | |
| 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 |
Downloads
Downloads per month over past year
Share and Export
Share and Export