Where academic tradition
meets the exciting future

You are here: TUCS > PUBLICATIONS > Publication Search > Supporting Reuse in Event B De...

Supporting Reuse in Event B Development: Modularisation Approach

Alexei Iliasov, Elena Troubitsyna, Linas Laibinis, Alexander Romanovsky, Kimmo Varpaaniemi, Dubravka Ilic, Timo Latvala, Supporting Reuse in Event B Development: Modularisation Approach. TUCS Technical Reports 947, Turku Centre for Computer Science, 2009.

Abstract:

Recently, Space Systems Finland has undertaken formal Event B development of
a part of on-board software for the BepiColombo space mission. As a result, lack
of modularisation mechanisms in Event B has been identified as a serious obstacle
to scalability. One of the main benefits of modularisation is that it allows us to
decompose system models into components that can be independently developed.
It also helps to manage complexity of models that in the industrial setting are usually
very large and difficult to comprehend. On the other hand, modularisation
enables reuse of formally developed components in the formal product line development.
In this paper we propose a conservative extension of Event B formalism
to support modularisation. We demonstrate how our approach can support reuse
in the formal development in the space domain.

Files:

Abstract in PDF-format

Full publication in PDF-format

BibTeX entry:

@TECHREPORT{tIlTrLaRoVaIlLa09a,
  title = {Supporting Reuse in Event B Development: Modularisation Approach},
  author = {Iliasov, Alexei and Troubitsyna, Elena and Laibinis, Linas and Romanovsky, Alexander and Varpaaniemi, Kimmo and Ilic, Dubravka and Latvala, Timo},
  number = {947},
  series = {TUCS Technical Reports},
  publisher = {Turku Centre for Computer Science},
  year = {2009},
  keywords = {Formal modelling, Event B, refinement, modularisation, reuse},
  ISBN = {978-952-12-2311-2},
}

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

Edit publication