Where academic tradition
meets the exciting future

You are here: TUCS > PUBLICATIONS > Publication Search > Developing Mode-Rich Satellite...

Developing Mode-Rich Satellite Software by Refinement in Event B

Alexei Iliasov, Elena Troubitsyna, Linas Laibinis, Alexander Romanovsky, Kimmo Varpaaniemi, Dubravka Ilic, Timo Latvala, Developing Mode-Rich Satellite Software by Refinement in Event B . In: Stefan Kowalewski, Marco Roveri (Eds.), Proceedings of FMICS 2010, the 15th International Workshop on Formal Methods for Industrial Critical Systems, Lecture Notes in Computer Science 6371, 50–66, Springer, 2010.

Abstract:

To ensure dependability of on-board satellite systems, the designers should, in particular,
guarantee correct implementation of the mode transition scheme, i.e., ensure that the states
of the system components are consistent with the global system mode. However, there is still
a lack of scalable approaches to formal verification of correctness of complex mode
transitions. In this paper we present a development of an Attitude and Orbit Control System
(AOCS) undertaken within the ICT DEPLOY project. AOCS is a complex mode-rich system,
which has an intricate mode-transition scheme. We show that refinement in Event-B provides
the engineers with a scalable formal technique that enables both development of mode-rich
systems and proof-based verification of their mode consistency.

BibTeX entry:

@INPROCEEDINGS{inpIlTrLaRoVaIlLa10b,
  title = {Developing Mode-Rich Satellite Software by Refinement in Event B },
  booktitle = {Proceedings of FMICS 2010, the 15th International Workshop on Formal Methods for Industrial Critical Systems},
  author = {Iliasov, Alexei and Troubitsyna, Elena and Laibinis, Linas and Romanovsky, Alexander and Varpaaniemi, Kimmo and Ilic, Dubravka and Latvala, Timo},
  volume = {6371},
  series = {Lecture Notes in Computer Science},
  editor = {Kowalewski, Stefan and Roveri, Marco},
  publisher = {Springer},
  pages = {50–66},
  year = {2010},
}

Belongs to TUCS Research Unit(s): Distributed Systems Laboratory (DS Lab)

Publication Forum rating of this publication: level 1

Edit publication