MURAL - Maynooth University Research Archive Library

    An Institution for Event-B

    Farrell, Marie and Monahan, Rosemary and Power, James F. (2017) An Institution for Event-B. In: Recent Trends in Algebraic Development Techniques : Revised Selected Papers. Lecture Notes in Computer Science (10644). Springer, Cham, Switzerland, pp. 104-119. ISBN 978-3-319-72043-2

    Download (1MB) | Preview

    Share your research

    Twitter Facebook LinkedIn GooglePlus Email more...

    Add this article to your Mendeley library


    This paper presents a formalisation of the Event-B formal specification language in terms of the theory of institutions. The main objective of this paper is to provide: (1) a mathematically sound semantics and (2) modularisation constructs for Event-B using the specification-building operations of the theory of institutions. Many formalisms have been improved in this way and our aim is thus to define an appropriate institution for Event-B, which we call EVT. We provide a definition of EVT and the proof of its satisfaction condition. A motivating example of a traffic-light simulation is presented to illustrate our approach.

    Item Type: Book Section
    Additional Information: This paper was presented at the 23rd IFIP WG 1.3 International Workshop, WADT 2016, Gregynog, UK, September 21–24, 2016.
    Keywords: Event-B; Institutions; Refinement; Formal methods; Modular specification; Formal specification;
    Academic Unit: Faculty of Science and Engineering > Computer Science
    Faculty of Science and Engineering > Research Institutes > Hamilton Institute
    Item ID: 12011
    Identification Number:
    Depositing User: Rosemary Monahan
    Date Deposited: 06 Dec 2019 12:15
    Publisher: Springer
    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