---
abstract: "Operation modes are useful structuring units that facilitate design of several safety-critical systems such as such as avionic, transportation and space systems. Although some support to the construction of modal systems can be found in the literature, modelling abstractions for the formal specification, analysis and correct construction of modal systems are still lacking. This paper discusses existing support for the construction of modal systems and proposes both a formalisation and a refinement notion for modal systems. A modal system, specified using the proposed abstractions, can be realised using different specification languages. Complementing the contribution, we define the requirements for an Event-B model to realise a modal system specification. A case study illustrates the proposed approach. \r\n"
accompaniment: []
book_title: ~
commentary: ~
completion_time: ~
composition_type: ~
conductors_id: []
conductors_name: []
contact_email: ~
copyright_holders: []
corp_creators: []
creators_id:
  - 'Fernando Luis Dotti <fernando.dotti@pucrs.br>'
  - '"Alexei Iliasov" <Alexei.Iliasov@newcastle.ac.uk>'
  - ~
  - alexander.romanovsky@ncl.ac.uk
creators_name:
  - family: Dotti
    given: Fernando
    honourific: ''
    lineage: ''
  - family: Iliasov
    given: Alexei
    honourific: ''
    lineage: ''
  - family: Riberiro
    given: Leila
    honourific: ''
    lineage: ''
  - family: Romanovsky
    given: Alexander
    honourific: ''
    lineage: ''
data_type: ~
date: 2009
date_type: published
datestamp: 2009-09-22 07:20:12
department: ~
dir: disk0/00/00/01/53
divisions: []
edit_lock_since: ~
edit_lock_until: ~
edit_lock_user: ~
editors_id: []
editors_name: []
eprint_status: archive
eprintid: 153
event_dates: 'December 9 -12, 2009'
event_location: 'Rio de Janeiro, Brazil'
event_title: 'International Conference on Formal Engineering Methods - ICFEM 09 '
event_type: conference
exhibitors_id: []
exhibitors_name: []
fileinfo: /style/images/fileicons/application_pdf.png;/153/1/paper105%2DICFEM09.pdf
full_text_status: public
funders: []
id_number: ~
importid: ~
institution: ~
isbn: ~
ispublished: pub
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-04-19 15:05:57
latitude: ~
learning_level: ~
longitude: ~
lyricists_id: []
lyricists_name: []
metadata_visibility: show
monograph_type: ~
note: ~
num_pieces: ~
number: ~
official_url: ~
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: 20
series: ~
skill_areas: []
source: ~
status_changed: 2009-09-22 07:20:12
subjects:
  - Refinement
  - deploy_method_comp
  - deploy_method_resil
succeeds: ~
suggestions: ~
sword_depositor: ~
sword_slug: ~
task_purpose: ~
thesis_type: ~
title: "Modal Systems: Specification, Refinement and Realisation\r\n"
type: conference_item
userid: 7
volume: ~
<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>