creators_name: Edmunds, Andrew
creators_name: Butler, Michael
type: conference_item
datestamp: 2011-05-06 13:17:45
lastmod: 2011-05-06 13:17:45
metadata_visibility: show
title: Tasking Event-B: An Extension to Event-B for Generating Concurrent Code
ispublished: pub
subjects: Event-Bsemantics
subjects: deploy_industrial
subjects: deploy_method
subjects: deploy_tooldev
full_text_status: public
pres_type: paper
keywords: Event-B, Code Generation, Tooling, Concurrency
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. 
date: 2011-02
date_type: published
event_title: PLACES 2011
event_type: workshop
refereed: TRUE
official_url: http://eprints.ecs.soton.ac.uk/22006/
citation:   Edmunds, Andrew and Butler, Michael  (2011) Tasking Event-B: An Extension to Event-B for Generating Concurrent Code.  In: PLACES 2011.     
document_url: http://deploy-eprints.ecs.soton.ac.uk/303/1/index.html