• TUCS Publication Series
• How to Publish in TUCS Series
• Publication Search
• Publication Graph
• Publication Input
• Publication Input Guide
• JuFo Browser

On Component-Based Reuse for Event-B

Andrew Edmunds, Marina Waldén, On Component-Based Reuse for Event-B. In: M. Butler, K.-D. Schewe, A. Mashkoor, M. Biro (Eds.), Abstract State Machines, Alloy, B, TLA, VDM, and Z, Lecture Notes in Computer Science 9675, 151–166, Springer, 2016.

http://dx.doi.org/10.1007/978-3-319-33600-8_9

Abstract:

Efficient reuse is a goal of many software engineering strategies and is useful 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 a component-based reuse strategy. In this paper, we outline a component-based reuse methodology for Event-B. It provides a means for bottom-up scalability, and can also be used with the existing top-down approach. We describe the process of creating library components, their composition, and specification of new properties (involving the composed elements). We introduce Event-B component interfaces and propose to use a diagrammatic representation of component instances (based on iUML-B) which can be used to describe the relationships between the composed elements. We also discuss the specification of communication flow across component boundaries and describe the additional proof obligations that are required.

BibTeX entry:

@INPROCEEDINGS{inpEdWa16a,
  title = {On Component-Based Reuse for Event-B},
  booktitle = {Abstract State Machines, Alloy, B, TLA, VDM, and Z},
  author = {Edmunds, Andrew and Waldén, Marina},
  volume = {9675},
  series = {Lecture Notes in Computer Science},
  editor = {Butler, M. and Schewe, K.-D. and Mashkoor, A. and Biro, M.},
  publisher = {Springer},
  pages = {151–166},
  year = {2016},
}

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

Edit publication