---
abstract: "In formal reasoning, modelling and proving activities are closely related. Models give rise to different proof obligations and information about failed proofs gives indications on how models should be improved. This document is  an attempt to address the latter issue: to understand how to deal with unprovable  obligations. We consider here proof obligations related to invariant preservation of an Event-B model: firstly, to understand the meaning of the proof obligations; secondly, to analyse various ways to fix the model accordingly. Our analysis is based on the concept of reachable states and inductive invariants.\r\n\r\nKeywords: Event-B, invariant, inductive invariant, proof obligations, modelling and proving. "
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: ''
data_type: ~
date: 2010-04
date_type: ~
datestamp: 2010-06-01 11:07:02
department: Department of Computer Science
dir: disk0/00/00/02/28
divisions: []
edit_lock_since: ~
edit_lock_until: 0
edit_lock_user: ~
editors_id: []
editors_name: []
eprint_status: archive
eprintid: 228
event_dates: ~
event_location: ~
event_title: ~
event_type: ~
exhibitors_id: []
exhibitors_name: []
fileinfo: ''
full_text_status: none
funders: []
id_number: 672
importid: ~
institution: Chair of Information Security
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-06-01 11:07:02
latitude: ~
learning_level: ~
longitude: ~
lyricists_id: []
lyricists_name: []
metadata_visibility: show
monograph_type: technical_report
note: ~
num_pieces: ~
number: ~
official_url: ftp://ftp.inf.ethz.ch/pub/publications/tech-reports/6xx/672.pdf
output_media: ~
pagerange: ~
pages: 16
patent_applicant: ~
pedagogic_type: ~
place_of_pub: Zurich
pres_type: ~
producers_id: []
producers_name: []
projects: []
publication: ~
publisher: 'ETH Zurich, Switzerland'
refereed: ~
referencetext: ~
related_url_type: []
related_url_url:
  - http://www.inf.ethz.ch/research/disstechreps/techreports
relation_type: []
relation_uri: []
rev_number: 8
series: ~
skill_areas: []
source: ~
status_changed: 2010-06-01 11:07:02
subjects:
  - deploy_training_eventb
succeeds: ~
suggestions: ~
sword_depositor: ~
sword_slug: ~
task_purpose: ~
thesis_type: ~
title: How to Interpret Failed Proofs in Event-B
type: monograph
userid: 16
volume: ~
<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>