Building Specifications in the Event-B Institution
| Autor: | Farrell, Marie, Monahan, Rosemary, Power, James F. |
|---|---|
| Rok vydání: | 2022 |
| Předmět: |
FOS: Computer and information sciences
Modularisation Computer Science - Logic in Computer Science General Computer Science Formal Languages and Automata Theory (cs.FL) Event-B Computer Science - Formal Languages and Automata Theory Refinement Institutions Formal Semantics Logic in Computer Science (cs.LO) Theoretical Computer Science |
| Zdroj: | Farrell, M, Monahan, R & Power, J F 2022, ' Building Specifications in the Event-B Institution ', Logical Methods in Computer Science, vol. 18, no. 4, pp. 4:1-4:55 . https://doi.org/10.46298/LMCS-18(4:4)2022 |
| ISSN: | 1860-5974 |
| DOI: | 10.46298/lmcs-18(4:4)2022 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|