---
abstract: "Event-B is a formal method which is widely used in modelling safety critical systems. So far, the main properties of interest in Event-B are safety related. Even though some liveness properties, e.g., termination, are already within the scope of Event-B, more general liveness properties, e.g. progress or persistence, are currently unsupported.  We present in this paper proof rules to reason about important classes of liveness properties. We\r\n illustrate our proof rules by applying them to prove liveness properties of realistic examples.  Our proof rules are based on several proof obligations that can be implemented in a tool support such as the Rodin platform.\r\n"
accompaniment: []
book_title: ~
commentary: ~
completion_time: ~
composition_type: ~
conductors_id: []
conductors_name: []
contact_email: ~
copyright_holders: []
corp_creators: []
creators_id:
  - htson@inf.ethz.ch
  - ~
creators_name:
  - family: Hoang
    given: Thai Son
    honourific: ''
    lineage: ''
  - family: Abrial
    given: Jean-Raymond
    honourific: ''
    lineage: ''
data_type: ~
date: ~
date_type: ~
datestamp: 2011-11-10 17:31:25
department: ~
dir: disk0/00/00/03/51
divisions: []
edit_lock_since: ~
edit_lock_until: 0
edit_lock_user: ~
editors_id: []
editors_name: []
eprint_status: archive
eprintid: 351
event_dates: ~
event_location: 'Durham, UK'
event_title: ICFEM 2011
event_type: conference
exhibitors_id: []
exhibitors_name: []
fileinfo: ''
full_text_status: none
funders: []
id_number: ~
importid: ~
institution: ~
isbn: ~
ispublished: pub
issn: ~
item_issues_comment: []
item_issues_count: ~
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-11-10 17:31:25
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: 9
series: ~
skill_areas: []
source: ~
status_changed: 2011-11-10 17:31:25
subjects:
  - deploy_method
  - theory
succeeds: ~
suggestions: ~
sword_depositor: ~
sword_slug: ~
task_purpose: ~
thesis_type: ~
title: Reasoning about Liveness in Event-B
type: conference_item
userid: 16
volume: ~
<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>