"143","A Code Generation Example for Event-B:  A Shared Channel with Concurrent Read/Writers","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.","http://deploy-eprints.ecs.soton.ac.uk/143/","Edmunds, Andrew and Butler, Michael","UNSPECIFIED","       <span class=\"person_name\">Edmunds, Andrew</span> and <span class=\"person_name\">Butler, Michael</span>     (2009)  <a href=\"http://deploy-eprints.ecs.soton.ac.uk/143/\"><em>A Code Generation Example for Event-B:&#13; A Shared Channel with Concurrent Read/Writers.</em></a>       [Rodin Archive]           ","ae2@ecs.soton.ac.uk,mjb@ecs.soton.ac.uk","2009"
<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>