---
abstract: 'Several safety-critical systems, such as avionic, transportation and space systems, use the notion of operation modes. Operation modes are useful structuring units that facilitate design, specially if used with state-based formal methods. However, modelling abstractions to support the specification, analysis and correct construction of modal systems are still lacking. The contribution of this paper is twofold: (i) modal systems and modal systems refinement are discussed and formalized; (ii) the relation of a modal system specification with an Event-B model is discussed, showing how to demonstrate that the behaviour of an Event-B model can satisfy a modal system.'
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: Romanovsky
    given: Alexander
    honourific: ''
    lineage: ''
data_type: ~
date: ~
date_type: ~
datestamp: 2009-07-08 15:31:36
department: ~
dir: disk0/00/00/01/34
divisions: []
edit_lock_since: ~
edit_lock_until: ~
edit_lock_user: ~
editors_id: []
editors_name: []
eprint_status: archive
eprintid: 134
event_dates: ' '
event_location: ' '
event_title: Newcastle University
event_type: other
exhibitors_id: []
exhibitors_name: []
fileinfo: /style/images/fileicons/application_pdf.png;/134/1/modesFM.pdf
full_text_status: public
funders: []
id_number: ~
importid: ~
institution: ~
isbn: ~
ispublished: unpub
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:56
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: (Technical report)
refereed: FALSE
referencetext: ~
related_url_type: []
related_url_url: []
relation_type: []
relation_uri: []
rev_number: 24
series: ~
skill_areas: []
source: ~
status_changed: 2009-07-08 15:31:36
subjects:
  - deploy_method_comp
  - deploy_method
  - Event-Bsemantics
succeeds: 132
suggestions: ~
sword_depositor: ~
sword_slug: ~
task_purpose: ~
thesis_type: ~
title: Specifying Modal Systems using Event-B
type: other
userid: 7
volume: ~
<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>