2 Challenges and Experiences in Formal Development of Onboard Software
2 Challenges and Experiences in Formal Development of Onboard Software
复制标题
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
A. Iliasov;E. Troubitsyna;L. Laibinis;A. Romanovsky;Kimmo Varpaaniemi;D. Ilic;T. Latvala
中科院分区：
文献类型：
--
作者：
A. Iliasov;E. Troubitsyna;L. Laibinis;A. Romanovsky;Kimmo Varpaaniemi;D. Ilic;T. Latvala
最近，芬兰空间系统公司为比佩科伦坡太空任务承担了部分星载软件的正式开发工作。因此，事件B中缺乏模块化机制已被认为是可伸缩性的严重障碍。模块化的主要好处之一是，它允许我们将系统模型分解成可以独立开发的组件。它还有助于管理在印度河试验环境中通常非常大和难以理解的模型的复杂性。另一方面，模块化允许在正式生产线开发中重用正式开发的组件。在这篇文章中，我们提出了事件B范式的保守扩展以支持模块化。我们演示了我们的方法如何支持空间领域的形式化开发中的重用。
Recently, Space Systems Finland has undertaken formal Even t B development of a part of on-board software for the BepiColombo spa ce mission. As a result, lack of modularization mechanisms in Event B has been i d t fied as a serious obstacle to scalability. One of the main benefits of modulari zation is that it allows us to decompose system models into components that can be indep e ntly developed. It also helps to manage complexity of models that in the indus trial setting are usually very large and difficult to comprehend. On the other hand, mod ularization enables reuse of formally developed components in the formal produc t line development. In this paper we propose a conservative extension of Event B f ormalism to support modularization. We demonstrate how our approach can suppor t reuse in the formal development in the space domain.