Share and Export
Share and Export
Farrell, Marie, 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
Preview
Monahan_Institution_LNCS_2017.pdf
Download (1MB) | Preview
Abstract
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: | 10.1007/978-3-319-72044-9_8 |
| Depositing User: | Rosemary Monahan |
| Date Deposited: | 06 Dec 2019 12:15 |
| Publisher: | Springer |
| Refereed: | Yes |
| Related URLs: | |
| URI: | https://mu.eprints-hosting.org/id/eprint/12011 |
| 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
Downloads
Downloads per month over past year
