Towards Component-based Reuse for Event-B

Andrew Edmunds, Marina Walden, Colin Snook

Tutkimustuotos: Artikkeli kirjassa/raportissa/konferenssijulkaisussaKonferenssiartikkeliTieteellinen


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.
AlkuperäiskieliEi tiedossa
OtsikkoProceedings of the 27th Nordic Workshop on Programming Theory, NWPT 2015
ToimittajatLuca Aceto, Ignacio Fabregas, Alvaro Garcia-Perez, Anna Ingolfsdottir
KustantajaReykjavik University, Iceland
TilaJulkaistu - 2016
OKM-julkaisutyyppiB3 Ei-soviteltu artikkeli konferenssin julkaisusarjassa
TapahtumaNordic Workshop on Programming Theory - 27th Nordic Workshop on Programming Theory, NWPT 2015
Kesto: 21 lokak. 201523 lokak. 2015


KonferenssiNordic Workshop on Programming Theory