---
abstract: "Ensuring system fault tolerance is one of the major concerns in developing critical industrial applications. The tutorial shows how to rigorously develop systems that are not only functionally correct but also fault tolerant. The material of the tutorial is built on the results of two EC projects, RODIN and DEPLOY, that created and validated in the industrial settings the RODIN platform - an Eclipse-based development environment supporting formal modelling in Event-B. The focus of the tutorial is on demonstrating how fault tolerance can be systematically specified and verified as an intrinsic part of the overall system behavior. The general principles are demonstrated by several industrial case studies based on our work with telecommunication, space and business information sectors. As part of the tutorial we will introduce and demonstrate a number of RODIN tools that support model structuring using modes, modules, and fault tolerance views, and facilitate fault tolerance modelling.\r\n\r\nAll materials of this tutorial are available on http://iliasov.org/fm2011/\r\n"
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>'
  - Linas.Laibinis@abo.fi
  - Elena.Troubitsyna@abo.fi
  - alexander.romanovsky@ncl.ac.uk
creators_name:
  - family: Iliasov
    given: Alexei
    honourific: ''
    lineage: ''
  - family: Laibinis
    given: Linas
    honourific: ''
    lineage: ''
  - family: Troubitsyna
    given: Elena
    honourific: ''
    lineage: ''
  - family: Romanovsky
    given: Alexander
    honourific: ''
    lineage: ''
data_type: ~
date: 2011
date_type: ~
datestamp: 2011-08-02 12:57:38
department: ~
dir: disk0/00/00/03/19
divisions: []
edit_lock_since: ~
edit_lock_until: 0
edit_lock_user: ~
editors_id: []
editors_name: []
eprint_status: archive
eprintid: 319
event_dates: ~
event_location: ~
event_title: ~
event_type: ~
exhibitors_id: []
exhibitors_name: []
fileinfo: ''
full_text_status: none
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: 2011-08-02 12:57:38
latitude: ~
learning_level: ~
longitude: ~
lyricists_id: []
lyricists_name: []
metadata_visibility: show
monograph_type: ~
note: ~
num_pieces: ~
number: ~
official_url: http://iliasov.org/fm2011/
output_media: ~
pagerange: ~
pages: ~
patent_applicant: ~
pedagogic_type: ~
place_of_pub: ~
pres_type: ~
producers_id: []
producers_name: []
projects: []
publication: ~
publisher: ~
refereed: ~
referencetext: ~
related_url_type: []
related_url_url:
  - http://sites.lero.ie/fm2011/Tutorial3.html
relation_type: []
relation_uri: []
rev_number: 10
series: ~
skill_areas: []
source: ~
status_changed: 2011-08-02 12:57:38
subjects:
  - Event-Bsemantics
  - Refinement
  - deploy_method
  - deploy_method_resil
  - deploy_training
succeeds: ~
suggestions: ~
sword_depositor: ~
sword_slug: ~
task_purpose: ~
thesis_type: ~
title: Correct-by-Construction Development of Fault Tolerant Systems (Tutorial at FM 2011)
type: teaching_resource
userid: 7
volume: ~
<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>