?url_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Adc&rft.title=A+Code+Generation+Example+for+Event-B%3A%0D%0AA+Shared+Channel+with+Concurrent+Read%2FWriters&rft.creator=Edmunds%2C+Andrew&rft.creator=Butler%2C+Michael&rft.subject=Tool+developments&rft.subject=Event-B&rft.description=We+present+an+example+involving+processes+reading+and+writing+to+a+shared+channel.+A+channel+may+have+at+most+one+reader+reading%2C+and+at+most+one+writer+writing+at+any+one+time%3B+however+a+number+of+processes+may+be+waiting+to+read+from%2C+or+write+to%2C+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%3B+and+a+read+event+constitutes%0D%0Amoving+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%2C+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%0D%0Awriter+having+to+complete+the+data+transfer.+We+continue+with+an+overview+of+our+implementation+notation+(OCB)%2C+and+show+the+implementation+level+specification+for+the+concurrent+read%2Fwriters+example.+We+then+present+details+of+the+implementation+level+refinement+that+results+from+the+translation+of+the+OCB+model+into+Event-B%2C+and+also+show+details+of+the+source+code+generated+by+the+Java+translator.&rft.date=2009&rft.type=Rodin+Archive&rft.type=NonPeerReviewed&rft.format=application%2Fpdf&rft.identifier=http%3A%2F%2Fdeploy-eprints.ecs.soton.ac.uk%2F143%2F2%2FRW2009SharedBufferExample.pdf&rft.format=application%2Fzip&rft.identifier=http%3A%2F%2Fdeploy-eprints.ecs.soton.ac.uk%2F143%2F3%2FSharedBufferExample.zip&rft.identifier=++Edmunds%2C+Andrew+and+Butler%2C+Michael++(2009)+A+Code+Generation+Example+for+Event-B%3A+A+Shared+Channel+with+Concurrent+Read%2FWriters.++%5BRodin+Archive%5D+++++&rft.relation=http%3A%2F%2Fdeploy-eprints.ecs.soton.ac.uk%2F143%2F<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>