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. Science of Computer Programming 78(7), 884–905, 2013.

http://dx.doi.org/10.1016/j.scico.2012.04.010

Abstract:

One of the guarantees that the designers of on-board satellite systems need to provide, so as to ensure their dependability, is that the mode transition scheme is implemented correctly, i.e. that the states of system components are consistent with the global system mode. There is still, however, a lack of scalable approaches to developing and verifying systems with complex mode transitions. This paper presents an approach to the formal development of mode-rich systems by refinement in Event-B. We formalise the concepts of modes and mode transitions as well as deriving specification and refinement patterns which support correct-by-construction system development. The proposed approach is validated by a formal development of the Attitude and Orbit Control System (AOCS) undertaken within the ICT DEPLOY project. The experience gained in the course of developing such a complex industrial system as AOCS, shows that Event-B refinement provides the engineers with a scalable formal technique. Moreover, the case study has demonstrated that Event-B can facilitate formal development of mode-rich systems and, in particular, proof-based verification of their mode consistency.

BibTeX entry:

@ARTICLE{jIlTrLaRoVaIlLa13a,
  title = {Developing Mode-Rich Satellite Software by Refinement in Event-B},
  author = {Iliasov, Alexei and Troubitsyna, Elena and Laibinis, Linas and Romanovsky, Alexander and Varpaaniemi, Kimmo and Ilic, Dubravka and Latvala, Timo},
  journal = {Science of Computer Programming},
  volume = {78},
  number = {7},
  publisher = {Elsevier},
  pages = {884–905},
  year = {2013},
  keywords = {Mode consistency; Event-B; Refinement; Components; Formal verification; On-board software},
}

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

Publication Forum rating of this publication: level 2

Edit publication