Towards Component-Based Reuse for Event-B

Andrew Edmunds, Colin Snook, Marina Walden

Tutkimustuotos: Kirja/lehti/raporttiTutkimusraporttiAmmatillinen

Abstrakti

A component-based system for Event-B would improve re-useability of Event-B machines, and also introduce the capability for bottom-up scalability. Tool support, and a theory underpinning composition, already exists. However, this is based on model decomposition, a top-down scalability solution. In that approach, the abstract model is refined by a composed-machine construct, that \emph{includes} the newly decomposed models. Decomposition has been used as a means to simplify complex models, or, for structural partitioning. The process of creating library components, their composition, and specification of new properties (of the composed elements) is relatively unexplored. In this paper we examine the issues surrounding component-based composition. We introduce the notion of Event-B component interfaces; we discuss communication flow across component boundaries, and what additional proofs obligations may be required; and we describe the tool support for supporting the new approach.
AlkuperäiskieliEnglanti
KustantajaTurku Centre for Computer Science (TUCS)
ISBN (painettu)978-952-12-3264-0
TilaJulkaistu - 2015
OKM-julkaisutyyppiD4 Julkaistut kehitykset tai tutkimusraportit tai tutkimukset

Julkaisusarja

NimiTUCS Technical Report
Vuosikerta1140

Sormenjälki

Sukella tutkimusaiheisiin 'Towards Component-Based Reuse for Event-B'. Ne muodostavat yhdessä ainutlaatuisen sormenjäljen.

Viittausmuodot