Developing Mode-Rich Satellite Software by Refinement in Event B

  1. Lookup NU author(s)
  2. Dr Alexei Iliasov
  3. Dr Elena Troubitsyna
  4. Professor Alexander Romanovsky
Author(s)Iliasov A, Troubitsyna E, Laibinis L, Romanovsky A, Varpaaniemi K, Ilic D, Latvala T
Publication type Report
Series TitleSchool of Computing Science Technical Report Series
Year2010
DateJune 2010
Report Number1207
Pages20
Full text is available for this publication:
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 complex mode-rich system, which has an intricate mode-transition scheme. We show that re 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.
InstitutionSchool of Computing Science, University of Newcastle upon Tyne
Place PublishedNewcastle upon Tyne
URLhttp://www.cs.ncl.ac.uk/publications/trs/papers/1207.pdf
ActionsLink to this publication