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

This is the latest version of this item.

Abstract

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.

Available Versions of this Item

• A Code Generation Example for Event-B: A Shared Channel with Concurrent Read/Writers. (deposited 31 Jul 2009 09:45)
  • A Code Generation Example for Event-B: A Shared Channel with Concurrent Read/Writers. (deposited 31 Jul 2009 10:10) [Currently Displayed]