BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//University of Liverpool Computer Science Seminar System//v2//EN
BEGIN:VEVENT
DTSTAMP:20260912T050607Z
UID:Seminar-verification-663@lxserverM.csc.liv.ac.uk
ORGANIZER:CN=Patrick Totzke:MAILTO:totzke@liverpool.ac.uk
DTSTART:20180412T140000
DTEND:20180412T150000
SUMMARY:Verification Series
DESCRIPTION:Marie Farrell: An Institution for Event-B: Clones, Modularisation and Interoperability\n\nIn 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.\n\nhttps://www.csc.liv.ac.uk/research/seminars/abstract.php?id=663
LOCATION:
END:VEVENT
END:VCALENDAR