---
abstract: 'Event-B is a formal modelling method which is claimed to be suitable for diverse modelling domains, such as reactive systems and sequential program development. This claim hinges on the fact that any particular model has an appropriate semantics. In Event-B this semantics is provided implicitly by proof obligations associated with a model. There is no fixed semantics though. In this article we argue that this approach is beneficial to modelling because we can use similar proof obligations across a variety of modelling domains. By way of two examples we show how similar proof obligations are linked to different semantics.  A small set of proof obligations is thus suitable for a whole range of modelling problems in diverse modelling domains.'
accompaniment: []
book_title: ~
commentary: ~
completion_time: ~
composition_type: ~
conductors_id: []
conductors_name: []
contact_email: ~
copyright_holders: []
corp_creators: []
creators_id:
  - sth@ecs.soton.ac.uk
creators_name:
  - family: Hallerstede
    given: Stefan
    honourific: ''
    lineage: ''
data_type: ~
date: 2008-06-31
date_type: published
datestamp: 2008-07-04 10:17:26
department: ~
dir: disk0/00/00/00/26
divisions: []
edit_lock_since: ~
edit_lock_until: ~
edit_lock_user: ~
editors_id: []
editors_name: []
eprint_status: archive
eprintid: 26
event_dates: September 2008
event_location: London
event_title: ABZ2008
event_type: conference
exhibitors_id: []
exhibitors_name: []
fileinfo: /style/images/fileicons/application_pdf.png;/26/1/evtbena.pdf
full_text_status: public
funders:
  - EU
id_number: ~
importid: ~
institution: ~
isbn: ~
ispublished: inpress
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:50
latitude: ~
learning_level: ~
longitude: ~
lyricists_id: []
lyricists_name: []
metadata_visibility: show
monograph_type: ~
note: ~
num_pieces: ~
number: ~
official_url: http://eprints.ecs.soton.ac.uk/16052/
output_media: ~
pagerange: ~
pages: ~
patent_applicant: ~
pedagogic_type: ~
place_of_pub: ~
pres_type: paper
producers_id: []
producers_name: []
projects:
  - DEPLOY
publication: ~
publisher: ~
refereed: TRUE
referencetext: ~
related_url_type: []
related_url_url: []
relation_type: []
relation_uri: []
rev_number: 20
series: ~
skill_areas: []
source: ~
status_changed: 2008-07-04 10:17:26
subjects:
  - Event-Bsemantics
succeeds: ~
suggestions: ~
sword_depositor: ~
sword_slug: ~
task_purpose: ~
thesis_type: ~
title: On the Purpose of Event-B Proof Obligations
type: conference_item
userid: 27
volume: ~
<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>