---
abstract: 'The Event-B method is a formal approach for modelling systems in safety-, and business-critical, domains. Initially, system specification takes place at a high level of abstraction; detail is added in refinement steps as the development proceeds toward implementation. Our aim has been to develop a novel approach for generating code, for concurrent programs, from Event-B. We formulated the approach so that it integrates well with the existing Event-B methodology and tools. In this paper we introduce a tasking extension for Event-B, with Tasking and Shared Machines. We make use of refinement, decomposition, and the extension, to structure projects for code generation for multitasking implementations. During the modelling phase decomposition is performed; decomposition reduces modelling complexity and makes proof more tractable. The decomposed models are then extended with sufficient information to enable generation of code. A task body describes a task?s behaviour, mainly using imperative, programming-like constructs. Task priority and life-cycle (periodic, triggered, etc.) are also specified, but timing aspects are not modelled formally. We provide tool support in order to validate the practical aspects of the approach. '
accompaniment: []
book_title: ~
commentary: ~
completion_time: ~
composition_type: ~
conductors_id: []
conductors_name: []
contact_email: ~
copyright_holders: []
corp_creators: []
creators_id: []
creators_name:
  - family: Edmunds
    given: Andrew
    honourific: ''
    lineage: ''
  - family: Butler
    given: Michael
    honourific: ''
    lineage: ''
data_type: ~
date: 2011-02
date_type: published
datestamp: 2011-05-06 13:17:45
department: ~
dir: disk0/00/00/03/03
divisions: []
edit_lock_since: ~
edit_lock_until: 0
edit_lock_user: ~
editors_id: []
editors_name: []
eprint_status: archive
eprintid: 303
event_dates: ~
event_location: ~
event_title: PLACES 2011
event_type: workshop
exhibitors_id: []
exhibitors_name: []
fileinfo: /style/images/fileicons/application_pdf.png;/303/1/index.html
full_text_status: public
funders:
  - Deploy
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: 'Event-B, Code Generation, Tooling, Concurrency'
lastmod: 2011-05-06 13:17:45
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/22006/
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: 27
series: ~
skill_areas: []
source: ~
status_changed: 2011-05-06 13:17:45
subjects:
  - Event-Bsemantics
  - deploy_industrial
  - deploy_method
  - deploy_tooldev
succeeds: ~
suggestions: ~
sword_depositor: ~
sword_slug: ~
task_purpose: ~
thesis_type: ~
title: 'Tasking Event-B: An Extension to Event-B for Generating Concurrent Code'
type: conference_item
userid: 187
volume: ~