Industrial deployment of system engineering methods providing high dependability and productivity


A Code Generation Example for Event-B: A Shared Channel with Concurrent Read/Writers

Edmunds, Andrew and Butler, Michael (2009) A Code Generation Example for Event-B: A Shared Channel with Concurrent Read/Writers. [Rodin Archive]

This is the latest version of this item.

PDF (A Shared Channel with Concurrent Read/Writers)
[img]ZIP Archive


We present an example involving processes reading and writing to a shared channel. A channel may have at most one reader reading, and at most one writer writing at any one time; however a number of processes may be waiting to read from, or write to, the channel. In our most abstract model data is transferred as a block in a single atomic step. A write event constitutes moving a block from a writing process to a channel buffer; and a read event constitutes moving a block from a channel buffer to a reader. The atomicity of the read and write activity is altered in the refinement - we introduce blocks that are made up of packets, and each packet is written to the channel individually. This allows the reader to begin reading as soon as there is data in the channel - without the writer having to complete the data transfer. We continue with an overview of our implementation notation (OCB), and show the implementation level specification for the concurrent read/writers example. We then present details of the implementation level refinement that results from the translation of the OCB model into Event-B, and also show details of the source code generated by the Java translator.

Item Type:Rodin Archive
Subjects:Tool developments
ID Code:143
Deposited By:Dr Andrew Edmunds
Deposited On:31 Jul 2009 10:10
Last Modified:08 Dec 2010 11:04

Available Versions of this Item

Repository Staff Only: item control page

Deploy-Project - All right reserved