Intranet Tools

nb. next round of REF2013 will be using data from eprints.ecs, but the central university REF interface.

RSS 1.0 Feed
RSS 2.0 Feed
Atom Feed
 

Tasking Event-B: An Extension to Event-B for Generating Concurrent Code

Edmunds, A. and Butler, M. (2011) Tasking Event-B: An Extension to Event-B for Generating Concurrent Code. In: PLACES 2011, 2nd April 2011, Saarbrucken, Germany.

Download

[img]
Preview
Accepted Version
PDF

227Kb

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.

Item Type:Conference or Workshop Item
Creator/Authors:
Andrew Edmunds
Michael Butler
Keywords:Event-B, Code Generation, Tooling, Concurrency
Research Group:Dependable Systems and Software Engineering Research Group
Date:09 February 2011
Information about this record:
Citations:
ID Code:22006
Last Modified:11 Apr 2011 10:20
Deposited On:10 Feb 2011 16:18 by Edmunds, Andrew

Tools & Metadata

Download Statistics

Last month

Last year

Members of ECS may view the download statistics dashboard for this record.

Corrections

ECS staff and postgraduates may modify this record

  Welcome from Deputy Head of School (Research) Research Prospectus Industrial Partnerships New Research Students Notes for Guidance New Research Students Notes for Guidance
The ECS EPrints Repository supports OAI 2.0 with a base URL of http://eprints.ecs.soton.ac.uk/cgi/oai2

EPrints is free software developed by the University of Southampton to facilitate Open Access to research.
EPrints