%0 Conference Proceedings
%T An Institution for Event-B
%+ National University of Ireland Maynooth (Maynooth University)
%A Farrell, Marie
%A Monahan, Rosemary
%A Power, James, F.
%Z Part 4: Regular Papers
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 23th International Workshop on Algebraic Development Techniques (WADT)
%C Gregynog, United Kingdom
%Y Phillip James
%Y Markus Roggenbach
%I Springer International Publishing
%3 Recent Trends in Algebraic Development Techniques
%V LNCS-10644
%P 104-119
%8 2016-09-21
%D 2016
%R 10.1007/978-3-319-72044-9_8
%K Event-B
%K Institutions
%K Refinement
%K Formal methods
%K Modular specification
%K Formal specification
%Z Computer Science [cs]Conference papers
%X 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 $$\mathcal {EVT}$$. We provide a definition of $$\mathcal {EVT}$$ and the proof of its satisfaction condition. A motivating example of a traffic-light simulation is presented to illustrate our approach.
%G English
%Z TC 1
%Z WG 1.3
%2 https://inria.hal.science/hal-01767469/document
%2 https://inria.hal.science/hal-01767469/file/433330_1_En_8_Chapter.pdf
%L hal-01767469
%U https://inria.hal.science/hal-01767469
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-TC1
%~ IFIP-WG1-3
%~ IFIP-WADT
%~ IFIP-LNCS-10644