The Formal Derivation of Mode Logic for Autonomous Satellite Flight Formation

Anton Tarasyuk, Inna Pereverzeva, Elena Troubitsyna, Timo Latvala

    Research output: Chapter in Book/Conference proceedingConference contributionScientificpeer-review

    Abstract

    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.
    Original languageUndefined/Unknown
    Title of host publicationComputer Safety, Reliability, and Security - 34th International Conference, SAFECOMP 2015, Delft, The Netherlands, September 23-25, 2015, Proceedings
    EditorsFloor Koornneef, Coen van Gulijk
    PublisherSpringer
    Pages29–43
    ISBN (Electronic)978-3-319-24254-5
    ISBN (Print)978-3-319-24254-5
    DOIs
    Publication statusPublished - 2015
    MoE publication typeA4 Article in a conference publication
    EventComputer Safety, Reliability, and Security (SAFECOMP) 2015 - 34th International Conference, SAFECOMP 2015
    Duration: 23 Sep 201525 Sep 2015

    Conference

    ConferenceComputer Safety, Reliability, and Security (SAFECOMP) 2015
    Period23/09/1525/09/15

    Keywords

    • Event-B
    • Formal modelling
    • Formal verification
    • Refinement

    Cite this