Towards Component-based Reuse for Event-B

Andrew Edmunds, Marina Walden, Colin Snook

Forskningsoutput: Kapitel i bok/konferenshandlingKonferensbidragVetenskaplig


An efficient re-use mechanism is a primary goal of many software development strategies; and is also important in the safety-critical domain, where formal development is required. Event-B can be used to develop safety-critical systems, but could be improved by development of a component-based re-use strategy. In this paper we outline a methodology, and the tool support required, for facilitating re-use of Event-B machines. As part of the ADVICeS project we are seeking to improve re-use of Event-B artefacts. The creation of a library of components, and a way to assemble them, would facilitate this. We propose to extend iUML-B class diagrams [9], and extend the composition techniques introduced in [7], to allow specification of Event-B components, interfaces, and composite components. Initial investigation has been undertaken as part of the project ADVICeS, funded by Academy of Finland, grant No. 266373. The approach also addresses the need, in Event-B, for bottom-up scalability. We describe the process of creating library components, their composition, and specification of new properties (of the composed elements). We introduce the notion of Event-B components, component interfaces, and composite components. We describe the additional annotations, and discuss composition invariants.
Titel på värdpublikationProceedings of the 27th Nordic Workshop on Programming Theory, NWPT 2015
RedaktörerLuca Aceto, Ignacio Fabregas, Alvaro Garcia-Perez, Anna Ingolfsdottir
FörlagReykjavik University, Iceland
StatusPublicerad - 2016
MoE-publikationstypB3 Ej refererad artikel i konferenshandlingar
EvenemangNordic Workshop on Programming Theory - 27th Nordic Workshop on Programming Theory, NWPT 2015
Varaktighet: 21 okt. 201523 okt. 2015


KonferensNordic Workshop on Programming Theory

Citera det här