Where academic tradition
meets the exciting future

You are here: TUCS > PUBLICATIONS > Publication Search > The Formal Derivation of Mode ...

The Formal Derivation of Mode Logic for Autonomous Satellite Flight Formation

Anton Tarasyuk, Inna Pereverzeva, Elena Troubitsyna, Timo Latvala, The Formal Derivation of Mode Logic for Autonomous Satellite Flight Formation. In: Floor Koornneef, Coen van Gulijk (Eds.), Computer Safety, Reliability, and Security (SAFECOMP), Lecture Notes in Computer Science 9337, 29–43, Springer International Publishing Switzerland, 2015.

http://dx.doi.org/10.1007/978-3-319-24255-2

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.

BibTeX entry:

@INPROCEEDINGS{inpTaPeTrLa15a,
  title = {The Formal Derivation of Mode Logic for Autonomous Satellite Flight Formation},
  booktitle = {Computer Safety, Reliability, and Security  (SAFECOMP)},
  author = {Tarasyuk, Anton and Pereverzeva, Inna and Troubitsyna, Elena and Latvala, Timo},
  volume = {9337},
  series = {Lecture Notes in Computer Science },
  editor = {Koornneef, Floor and Gulijk, Coen van},
  publisher = {Springer International Publishing Switzerland},
  pages = {29–43},
  year = {2015},
  keywords = {Vormal modelling, Refinement, Formal verification, Event-B},
}

Belongs to TUCS Research Unit(s): Embedded Systems Laboratory (ESLAB)

Publication Forum rating of this publication: level 1

Edit publication