?url_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Adc&rft.title=On+Event-B+and+Control+Flow+%0D%0A&rft.creator=Iliasov%2C+Alexei&rft.subject=Event-B&rft.subject=Code+generation&rft.description=Event-B+is+a+general+purpose+formal+development+method+%0D%0Asuitable+for+the+design+and+detailed+development+of+safety-critical+systems.+Being+a+data-driven+formalism%2C+it+lacks+any+control+%EF%AC%82ow+constructs.+This+turns+out+to+be+a+limitation+for+systems+with+rich+control+%EF%AC%82ow+properties.+In+Event-B%2C+control+%EF%AC%82ow+information+has+to+be+embedded+into+%0D%0Aguards+and+event+actions+and+this+results+in+an+entanglement+of+control+%EF%AC%82ow+and+functional+specification+with+the+additional+downside+of+extra+model+variables.+This+paper+proposes+a+method+for+extending+Event-B++models+with+an+new+viewpoint+portraying+control+%EF%AC%82ow+properties+of+a+%0D%0Amodel.+The+novelty+of+the+work+is+in+relying+solely+on+theorem+proving+to+demonstrate+the+consistency+of+control+%EF%AC%82ow+and+main+Event-B+specification.+The+focus+is+placed+on+the+practicality+of+working+with+such++an+extension+and+also+on+achieving+proof+economy.+A+detailed+formal+%0D%0Atreatment+of+the+method+is+presented+and+illustrated+with+a+case+study.++A+proof+of+concept+implementation+for+the+RODIN+platform+is+brie%EF%AC%82y+discussed.+%0D%0A&rft.publisher=DEPLOY+Project&rft.date=2009&rft.type=Other&rft.type=NonPeerReviewed&rft.format=application%2Fpdf&rft.identifier=http%3A%2F%2Fdeploy-eprints.ecs.soton.ac.uk%2F144%2F1%2Fflows-paper..pdf&rft.identifier=++Iliasov%2C+Alexei++(2009)+On+Event-B+and+Control+Flow.++DEPLOY+Project.++++(Unpublished)++&rft.relation=http%3A%2F%2Fdeploy-eprints.ecs.soton.ac.uk%2F144%2F<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>