An Institution for Event-B: Clones, Modularisation and Interoperability

12^th April 2018, 14:00
Marie Farrell

Abstract

In this talk I will discuss some of the work completed during my PhD research which centred on the definition of an institution for the Event-B formal specification language. The theory of institutions observes that once the syntax and semantics of a formal system have been defined in a uniform way, using some basic constructs from category theory, then a set of specification-building operators can be defined that allow you to write, modularise and build up specifications in a formalism-independent manner. We have represented the Event-B formalism as an institution called EVT and have thus provided modularisation constructs which increase the scalability of Event-B for use in larger projects. In order to motivate the need for such modularisation constructs in Event-B we have conducted an empirical study of the occurrence of event and machine clones throughout a large corpus of Event-B specifications (containing both simple and industrial-scale examples). Another benefit of this approach is the increased interoperability of Event-B via institution comorphisms which will allow aspects of the system be specified in different formalisms and included in the final Event-B specification. The Event-B formalism was not equipped with a formally defined semantics and this approach has enabled us to define a translational semantics for Event-B by translating Event-B specifications to specifications written in the language of the EVT institution.