Marie Farrell ; Rosemary Monahan ; James F. Power - Building Specifications in the Event-B Institution

lmcs:7286 - Logical Methods in Computer Science, November 9, 2022, Volume 18, Issue 4 - https://doi.org/10.46298/lmcs-18(4:4)2022
Building Specifications in the Event-B Institution

Authors: Marie Farrell ; Rosemary Monahan ; James F. Power

    This paper describes a formal semantics for the Event-B specification language using the theory of institutions. We define an institution for Event-B, EVT, and prove that it meets the validity requirements for satisfaction preservation and model amalgamation. We also present a series of functions that show how the constructs of the Event-B specification language can be mapped into our institution. Our semantics sheds new light on the structure of the Event-B language, allowing us to clearly delineate three constituent sub-languages: the superstructure, infrastructure and mathematical languages. One of the principal goals of our semantics is to provide 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. We have implemented our approach via a parser and translator for Event-B specifications, EBtoEVT, which also provides a gateway to the Hets toolkit for heterogeneous specification.


    Volume: Volume 18, Issue 4
    Published on: November 9, 2022
    Accepted on: September 28, 2022
    Submitted on: March 22, 2021
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Formal Languages and Automata Theory

    Share

    Consultation statistics

    This page has been seen 435 times.
    This article's PDF has been downloaded 296 times.