Toggle Main Menu Toggle Search

Open Access padlockePrints

Developing Mode-Rich Satellite Software by Refinement in Event B

Lookup NU author(s): Dr Alexei Iliasov, Dr Elena Troubitsyna, Professor Alexander Romanovsky

Downloads


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 formal 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.


Publication metadata

Author(s): Iliasov A, Troubitsyna E, Laibinis L, Romanovsky A, Varpaaniemi K, Ilic D, Latvala T

Editor(s): Kowalewski, S., Roveri, M.

Publication type: Conference Proceedings (inc. Abstract)

Publication status: Published

Conference Name: Formal Methods for Industrial Critical Systems: 15th International Workshop (FMICS)

Year of Conference: 2010

Pages: 50-66

ISSN: 0302-9743 (print) 1611-3349 (online)

Publisher: Springer

URL: http://dx.doi.org/10.1007/978-3-642-15898-8_4

DOI: 10.1007/978-3-642-15898-8_4

Library holdings: Search Newcastle University Library for this item

Series Title: Lecture Notes in Computer Science

ISBN: 9783642158971


Actions

Find at Newcastle University icon    Link to this publication


Share