---
abstract: "To ensure dependability of on-board satellite systems, the\r\ndesigners 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."
accompaniment: []
book_title: ~
commentary: ~
completion_time: ~
composition_type: ~
conductors_id: []
conductors_name: []
contact_email: ~
copyright_holders: []
corp_creators: []
creators_id:
  - '"Alexei Iliasov" <Alexei.Iliasov@newcastle.ac.uk>'
  - Elena.Troubitsyna@abo.fi
  - Linas.Laibinis@abo.fi
  - alexander.romanovsky@ncl.ac.uk
  - ~
  - ~
  - ~
creators_name:
  - family: Iliasov
    given: Alexei
    honourific: ''
    lineage: ''
  - family: Troubitsyna
    given: Elena
    honourific: ''
    lineage: ''
  - family: Laibinis
    given: Linas
    honourific: ''
    lineage: ''
  - family: Romanovsky
    given: Alexander
    honourific: ''
    lineage: ''
  - family: Varpaaniemi
    given: Kimmo
    honourific: ''
    lineage: ''
  - family: Ilic
    given: Dubravka
    honourific: ''
    lineage: ''
  - family: Latvala
    given: Timo
    honourific: ''
    lineage: ''
data_type: ~
date: 2010
date_type: published
datestamp: 2010-07-14 13:04:50
department: ~
dir: disk0/00/00/02/40
divisions: []
edit_lock_since: ~
edit_lock_until: 0
edit_lock_user: ~
editors_id: []
editors_name: []
eprint_status: archive
eprintid: 240
event_dates: 'September 20-21, 2010'
event_location: 'Antwerp, Belgium'
event_title: 15th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2010)
event_type: conference
exhibitors_id: []
exhibitors_name: []
fileinfo: /style/images/fileicons/application_pdf.png;/240/1/FMICS_CR.pdf
full_text_status: restricted
funders: []
id_number: ~
importid: ~
institution: ~
isbn: ~
ispublished: inpress
issn: ~
item_issues_comment: []
item_issues_count: 0
item_issues_description: []
item_issues_id: []
item_issues_reported_by: []
item_issues_resolved_by: []
item_issues_status: []
item_issues_timestamp: []
item_issues_type: []
keywords: ~
lastmod: 2010-07-14 13:13:09
latitude: ~
learning_level: ~
longitude: ~
lyricists_id: []
lyricists_name: []
metadata_visibility: show
monograph_type: ~
note: ~
num_pieces: ~
number: ~
official_url: https://es.fbk.eu/events/fmics2010/index.php
output_media: ~
pagerange: ~
pages: ~
patent_applicant: ~
pedagogic_type: ~
place_of_pub: ~
pres_type: paper
producers_id: []
producers_name: []
projects: []
publication: ~
publisher: ~
refereed: TRUE
referencetext: ~
related_url_type: []
related_url_url: []
relation_type: []
relation_uri: []
rev_number: 36
series: ~
skill_areas: []
source: ~
status_changed: 2010-07-14 13:13:09
subjects:
  - Event-Bsemantics
  - deploy_industrial_space
  - deploy_method_comp
  - deploy_method_resil
  - deploy_tooldev_modelc
  - deploy_tooldev_rodinplugins
succeeds: ~
suggestions: ~
sword_depositor: ~
sword_slug: ~
task_purpose: ~
thesis_type: ~
title: Developing Mode-Rich Satellite Software by Refinement in Event B
type: conference_item
userid: 7
volume: ~
<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>