Iliasov, Alexei and Troubitsyna, Elena and Laibinis, Linas and Romanovsky, Alexander and Varpaaniemi, Kimmo and Ilic, Dubravka and Latvala, Timo Supporting Reuse in Event B Development: Modularisation Approach. Aabo Akademi, Finland. (Unpublished)
This is the latest version of this item.
![[img]](../style/images/fileicons/application_pdf.png)
| PDF 250Kb |
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 modularization mechanisms in Event B has been identified as a serious obstacle to scalability. One of the main benefit of modularization 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, modularization 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 modularization. We demonstrate how our approach can support reuse in the formal development in the space domain.
| Item Type: | Other |
|---|---|
| Subjects: | Industrial Deployment > Space Methodology > Composition and reuse Methodology Event-B Industrial Deployment |
| ID Code: | 159 |
| Deposited By: | Prof A Romanovsky |
| Deposited On: | 14 Oct 2009 11:25 |
| Last Modified: | 19 Apr 2010 16:05 |
Available Versions of this Item
- Supporting Reuse in Event B Development: Modularisation Approach. (deposited 06 May 2009 11:50)
- Supporting Reuse in Event B Development: Modularisation Approach. (deposited 14 Oct 2009 11:25) [Currently Displayed]
Repository Staff Only: item control page
