TY - INPR ID - deploy240 UR - https://es.fbk.eu/events/fmics2010/index.php A1 - Iliasov, Alexei A1 - Troubitsyna, Elena A1 - Laibinis, Linas A1 - Romanovsky, Alexander A1 - Varpaaniemi, Kimmo A1 - Ilic, Dubravka A1 - Latvala, Timo Y1 - 2010/// N2 - 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 re?finement 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. TI - Developing Mode-Rich Satellite Software by Refinement in Event B AV - restricted M2 - Antwerp, Belgium T2 - 15th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2010) ER -