MURAL - Maynooth University Research Archive Library



    Building Specifications in the Event-B Institution: A Summary


    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

    [thumbnail of MarieFarrellEventB2021.pdf]
    Preview
    Text
    MarieFarrellEventB2021.pdf

    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:
    URI: https://mural.maynoothuniversity.ie/id/eprint/18574
    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
    Item control page

    Downloads

    Downloads per month over past year

    Origin of downloads