?url_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Adc&rft.title=Redevelopment+of+an+Industrial+Case+Study+Using+Event-B+and+Rodin&rft.creator=Rezazadeh%2C+Abdolbaghi&rft.creator=Butler%2C+Michael&rft.creator=Evans%2C+Neil&rft.subject=Other&rft.subject=Refinement&rft.subject=Event-B+Examples&rft.description=CDIS+is+a+commercial+air+traffic+information+system+that+was+developed+using+formal+methods+15+years+ago+by+Praxis%2C+and+it+is+still+in+operation+today.+This+system+is+an+example+of+an+industrial+scale+system+that+has+been+developed+using+formal+methods.+In+particular%2C+the+functional+requirements+of+the+system+were+specified+using+VVSL+--+a+variant+of+VDM.+A+subset+of+the+original+specification+has+been+chosen+to+be+reconstructed+on+the+Rodin+platform+based+on+the+new+Event-B+formalism.+The+goal+of+our+reconstruction+was+to+overcome+three+key+difficulties+of+the+original+formalisation%2C+namely+the+difficulty+of+comprehending+the+original+specification%2C+the+lack+of+any+mechanical+proof+of+the+consistency+of+the+specification+and+the+difficulty+of+dealing+with+distribution+and+atomicity+refinement.+In+this+paper+we+elucidate+how+a+new+formal+notation+and+tool+can+help+to+overcome+these+difficulties.&rft.date=2007-12-17&rft.type=Rodin+Archive&rft.type=PeerReviewed&rft.format=application%2Fpdf&rft.identifier=http%3A%2F%2Fdeploy-eprints.ecs.soton.ac.uk%2F9%2F1%2FRedevelopment_of_an_Industrial_Case_Study_Using_Event-B_and_Rodin.pdf&rft.format=application%2Fzip&rft.identifier=http%3A%2F%2Fdeploy-eprints.ecs.soton.ac.uk%2F9%2F2%2FCDIS-19-NOV-07.zip&rft.identifier=++Rezazadeh%2C+Abdolbaghi+and+Butler%2C+Michael+and+Evans%2C+Neil++(2007)+Redevelopment+of+an+Industrial+Case+Study+Using+Event-B+and+Rodin.++%5BRodin+Archive%5D++++(In+Press)++&rft.relation=http%3A%2F%2Fdeploy-eprints.ecs.soton.ac.uk%2F9%2F<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>