The Formal Derivation of Mode Logic for Autonomous Satellite Flight Formation
The Formal Derivation of Mode Logic for Autonomous Satellite Flight Formation
复制标题
卫星自主飞行编队模式逻辑的形式化推导
DOI：
10.1007/978-3-319-24255-2_4
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
T. Latvala
中科院分区：
文献类型：
--
作者：
A. Tarasyuk;Inna Pereverzeva;E. Troubitsyna;T. Latvala
卫星编队飞行是自主分布式系统的一个例子，它依赖于复杂的协调模式转换来完成其使命。虽然该技术有望带来重大的经济和科学效益，但它也构成了一个重大的核查挑战，因为不可能在地面测试该系统。在本文中，我们的实验与形式化建模和基于证明的验证，以获得模式逻辑的自主飞行编队。我们依靠事件B和基于证明的验证中的细化来创建实现协调模式转换的自主操作的详细规范。通过对系统级模型的分解，推导出了卫星间的接口，保证了在通信信道不可靠的情况下，卫星间的通信支持正确的模式转换。我们认为，本文所倡导的正式系统的方法构成了一个坚实的基础，设计复杂的自治系统。
Satellite formation flying is an example of an autonomous distributed system that relies on complex coordinated mode transitions to accomplish its mission. While the technology promises significant economical and scientific benefits, it also poses a major verification challenge since testing the system on the ground is impossible. In this paper, we experiment with formal modelling and proof-based verification to derive mode logic for autonomous flight formation. We rely on refinement in Event-B and proof-based verification to create a detailed specification of the autonomic actions implementing the coordinated mode transitions. By decomposing system-level model, we derive the interfaces of the satellites and guarantee that their communication supports correct mode transitions despite unreliability of the communication channel. We argue that a formal systems approach advocated in this paper constitutes a solid basis for designing complex autonomic systems.