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