Supporting Reuse in Event B Development: Modularisation Approach
| Autor: | Linas Laibinis, Elena Troubitsyna, Alexei Iliasov, Alexander Romanovsky, Timo Latvala, Kimmo Varpaaniemi, Dubravka Ilic |
|---|---|
| Rok vydání: | 2010 |
| Předmět: |
Engineering
business.industry Industrial setting 020207 software engineering 02 engineering and technology Reuse Software Conservative extension Obstacle Product line Scalability 0202 electrical engineering electronic engineering information engineering Systems engineering 020201 artificial intelligence & image processing Formal development business |
| Zdroj: | Abstract State Machines, Alloy, B and Z ISBN: 9783642118104 ASM |
| DOI: | 10.1007/978-3-642-11811-1_14 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|