creators_name: Iliasov, Alexei creators_name: Troubitsyna, Elena creators_name: Laibinis, Linas creators_name: Romanovsky, Alexander creators_name: Varpaaniemi, Kimmo creators_name: Ilic, Dubravka creators_name: Latvala, Timo creators_id: "Alexei Iliasov" creators_id: Elena.Troubitsyna@abo.fi creators_id: Linas.Laibinis@abo.fi creators_id: alexander.romanovsky@ncl.ac.uk type: conference_item datestamp: 2010-07-14 13:04:50 lastmod: 2010-07-14 13:13:09 metadata_visibility: show title: Developing Mode-Rich Satellite Software by Refinement in Event B ispublished: inpress subjects: Event-Bsemantics subjects: deploy_industrial_space subjects: deploy_method_comp subjects: deploy_method_resil subjects: deploy_tooldev_modelc subjects: deploy_tooldev_rodinplugins full_text_status: restricted pres_type: paper 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 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. date: 2010 date_type: published event_title: 15th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2010) event_location: Antwerp, Belgium event_dates: September 20-21, 2010 event_type: conference refereed: TRUE official_url: https://es.fbk.eu/events/fmics2010/index.php citation: Iliasov, Alexei and Troubitsyna, Elena and Laibinis, Linas and Romanovsky, Alexander and Varpaaniemi, Kimmo and Ilic, Dubravka and Latvala, Timo (2010) Developing Mode-Rich Satellite Software by Refinement in Event B. In: 15th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2010), September 20-21, 2010, Antwerp, Belgium. (In Press) document_url: http://deploy-eprints.ecs.soton.ac.uk/240/1/FMICS_CR.pdf