creators_name: Iliasov, Alexei creators_name: Troubitsyna, Elena creators_name: Laibinis, Linas creators_name: Romanovsky, Alexander creators_name: Varpaaniemi, Kimmo creators_name: Ilic, Dubravka creators_name: Latvala, Timo creators_id: "Alexei Iliasov" creators_id: Elena.Troubitsyna@abo.fi creators_id: Linas.Laibinis@abo.fi creators_id: alexander.romanovsky@ncl.ac.uk type: conference_item datestamp: 2010-01-11 08:48:50 lastmod: 2010-04-19 15:05:59 metadata_visibility: show title: Supporting Reuse in Event B Development: Modularisation Approach ispublished: pub subjects: Event-Bsemantics subjects: Refinement subjects: deploy_industrial_space subjects: deploy_method_comp subjects: deploy_tooldev_rodinplugins full_text_status: public pres_type: paper 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 benifits 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. date: 2010 date_type: published pagerange: 174-188 event_title: Abstract State Machines (ASM), Alloy, B and Z Conference (ABZ 2010) event_location: Orford, Québec, Canada event_dates: February 22-25, 2010 event_type: conference refereed: TRUE citation: Iliasov, Alexei and Troubitsyna, Elena and Laibinis, Linas and Romanovsky, Alexander and Varpaaniemi, Kimmo and Ilic, Dubravka and Latvala, Timo (2010) Supporting Reuse in Event B Development: Modularisation Approach. In: Abstract State Machines (ASM), Alloy, B and Z Conference (ABZ 2010), February 22-25, 2010, Orford, Québec, Canada. document_url: http://deploy-eprints.ecs.soton.ac.uk/172/1/Modules_paper-submitted.pdf