MURAL - Maynooth University Research Archive Library

    Building Specifications in the Event-B Institution: A Summary

    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

    [img] Download (705kB)

    Share your research

    Twitter Facebook LinkedIn GooglePlus Email more...

    Add this article to your Mendeley library


    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:
    Depositing User: Marie Farrell
    Date Deposited: 23 May 2024 11:43
    Journal or Publication Title: Rigorous State-Based Methods
    Publisher: springer link
    Refereed: Yes
    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)

    View Item Item control page


    Downloads per month over past year

    Origin of downloads