Conference Publication Details
Mandatory Fields
Farrell M.;Monahan R.;Power J.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
An institution for event-B
2017
January
Published
1
()
Optional Fields
Event-B Formal methods Formal specification Institutions Modular specification Refinement
104
119
© IFIP International Federation for Information Processing 2017 Published by Springer International Publishing AG 2017. All Rights Reserved. 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 ɛVT. We provide a definition of ɛVT and the proof of its satisfaction condition. A motivating example of a traffic-light simulation is presented to illustrate our approach.
10.1007/978-3-319-72044-9_8
Grant Details