---
abstract: "Event-B is a general purpose formal development method \r\nsuitable for the design and detailed development of safety-critical systems. Being a data-driven formalism, it lacks any control flow constructs. This turns out to be a limitation for systems with rich control flow properties. In Event-B, control flow information has to be embedded into \r\nguards and event actions and this results in an entanglement of control flow and functional specification with the additional downside of extra model variables. This paper proposes a method for extending Event-B  models with an new viewpoint portraying control flow properties of a \r\nmodel. The novelty of the work is in relying solely on theorem proving to demonstrate the consistency of control flow and main Event-B specification. The focus is placed on the practicality of working with such  an extension and also on achieving proof economy. A detailed formal \r\ntreatment of the method is presented and illustrated with a case study.  A proof of concept implementation for the RODIN platform is briefly discussed. \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>'
creators_name:
  - family: Iliasov
    given: Alexei
    honourific: ''
    lineage: ''
data_type: ~
date: 2009
date_type: ''
datestamp: 2009-08-11 16:17:31
department: ~
dir: disk0/00/00/01/44
divisions: []
edit_lock_since: ~
edit_lock_until: ~
edit_lock_user: ~
editors_id: []
editors_name: []
eprint_status: archive
eprintid: 144
event_dates: ~
event_location: ~
event_title: ~
event_type: ~
exhibitors_id: []
exhibitors_name: []
fileinfo: /style/images/fileicons/application_pdf.png;/144/1/flows%2Dpaper..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:57
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: ~
producers_id: []
producers_name: []
projects: []
publication: ~
publisher: DEPLOY Project
refereed: ~
referencetext: ~
related_url_type: []
related_url_url: []
relation_type: []
relation_uri: []
rev_number: 18
series: ~
skill_areas: []
source: ~
status_changed: 2009-08-11 16:17:31
subjects:
  - Event-Bsemantics
  - Code_generation
succeeds: ~
suggestions: ~
sword_depositor: ~
sword_slug: ~
task_purpose: ~
thesis_type: ~
title: "On Event-B and Control Flow \r\n"
type: other
userid: 7
volume: ~
<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>