Where academic tradition
meets the exciting future

Towards Component-Based Reuse for Event-B

Andrew Edmunds, Marina Walden, Colin Snook, Towards Component-Based Reuse for Event-B. In: Luca Aceto, Anna Ingolfsdottir (Eds.), Proceedings of the 27th Nordic Workshop on Programming Theory, 1–3, Reykjavik University, Iceland, 2015.

Abstract:

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.

BibTeX entry:

@INPROCEEDINGS{inpEdWaSn16a,
  title = {Towards Component-Based Reuse for Event-B},
  booktitle = {Proceedings of the 27th Nordic Workshop on Programming Theory},
  author = {Edmunds, Andrew and Walden, Marina and Snook, Colin},
  editor = {Aceto, Luca and Ingolfsdottir, Anna},
  publisher = {Reykjavik University, Iceland},
  pages = {1–3},
  year = {2015},
}

Belongs to TUCS Research Unit(s): Distributed Systems Laboratory (DS Lab)

Edit publication