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.
If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.
% BibTex
@inproceedings{IliasovTLRVIL10,
author = {Alexei Iliasov and
Elena Troubitsyna and
Linas Laibinis and
Alexander B. Romanovsky and
Kimmo Varpaaniemi and
Dubravka Ilic and
Timo Latvala},
editor = {Marc Frappier and
Uwe Gl{\"{a}}sser and
Sarfraz Khurshid and
R{\'{e}}gine Laleau and
Steve Reeves},
title = {Supporting Reuse in Event {B} Development: Modularisation Approach},
booktitle = {Abstract State Machines, Alloy, {B} and Z, Second International Conference,
{ABZ} 2010, Orford, QC, Canada, February 22-25, 2010. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5977},
pages = {174--188},
publisher = {Springer},
year = {2010},
url = {https://doi.org/10.1007/978-3-642-11811-1\_14},
doi = {10.1007/978-3-642-11811-1\_14},
timestamp = {Mon, 05 Feb 2024 20:35:41 +0100},
biburl = {https://dblp.org/rec/conf/asm/IliasovTLRVIL10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}