Where academic tradition
meets the exciting future

Supporting Reuse in Event B Development: Modularisation Approach

Alexei Iliasov, Elena Troubitsyna, Linas Laibinis, Alexander Romanovsky, Kimmo Varpaaniemi, Dubravka Ilic, Timmo Latvala, Supporting Reuse in Event B Development: Modularisation Approach. In: Marc Frappier, Uwe Glässer, Sarfraz Khurshid, Régine Laleau, Steve Reeves (Eds.), Proceedings of ABZ 2010, Lecture Notes in Computer Science 5977, 174–188, Springer, 2010.

http://dx.doi.org/10.1007/978-3-642-11811-1_14

Abstract:

Recently, Space Systems Finland has undertaken formal Event B development of a part of
the 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.

BibTeX entry:

@INPROCEEDINGS{inpIlTrLaRoVaIlLa10a,
  title = {Supporting Reuse in Event B Development: Modularisation Approach},
  booktitle = {Proceedings of ABZ 2010},
  author = {Iliasov, Alexei and Troubitsyna, Elena and Laibinis, Linas and Romanovsky, Alexander and Varpaaniemi, Kimmo and Ilic, Dubravka and Latvala, Timmo},
  volume = {5977},
  series = {Lecture Notes in Computer Science},
  editor = {Frappier, Marc and Glässer, Uwe and Khurshid, Sarfraz and Laleau, Régine and Reeves, Steve},
  publisher = {Springer},
  pages = {174–188},
  year = {2010},
}

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

Publication Forum rating of this publication: level 1

Edit publication