?url_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Adc&rft.title=PhD+Thesis%3A+Formal+Construction+of+Instruction+Set+Architectures&rft.creator=Wright%2C+Stephen&rft.subject=Event-B&rft.subject=Methodology&rft.subject=Tool+developments&rft.description=The+Instruction+Set+Architecture+(ISA)+is+that+part+of+a+computing+machine+visible+for+programming%2C+including+its+native+data+types%2C+instructions%2C+registers%2C+memory+architecture%2C+exception+handling+and+external+interfaces.+The+ISA+also+includes+the+specification+of+the+machine%E2%80%99s+native+language%3A+that+is+its+instructions+and+their+actions.+This+thesis+proposes+the+use+of+the+Event-B+formal+notation+to+construct+a+sequence+of+formal+specifications+applicable+to+a+range+of+ISAs%2C+by+abstractly+capturing+their+shared+properties.+Initial%2C+very+abstract%2C+descriptions+are+refined+by+the+incremental+addition+of+greater+detail%2C+each+increment+providing+a+template+for+development+of+the+next.+The+use+of+Event-B+allows+correctness%2C+i.e.+the+preservation+of+the+properties+of+the+previous+step%2C+to+be+verified+over+successive+refinements.+This+is+achieved+by+the+creation+and+proving+of+logical+hypotheses%2C+or+proof+obligations.%0D%0A%0D%0AThe+process+enables+development+of+ISAs+with+predictable+behaviour+when+executing+both+correct+and+erroneous+programs%2C+by+identification+of+the+precise+preconditions+required+for+successful+execution+of+instructions%2C+their+resulting+actions%2C+and+all+possible+error+conditions.+Application+of+property+proving+techniques+allows+for+the+formal+verification+of+desirable+properties.%0D%0A%0D%0AA+methodology+is+proposed+for+the+incremental+construction+of+the+common+elements+of+an+ISA%2C+and+its+features+are+discussed.+The+methodology+is+initially+used+to+construct+a+generic+description%2C+which+is+then+demonstrated+by+refinement+to+two+representative+ISAs+capable+of+executing+compiled+C+binary+executables.+The+complete+refinement+process+is+demonstrated+by+the+creation+and+testing+of+Virtual+Machines+automatically+generated+via+novel+translation+tools.%0D%0A%0D%0APrior+art+has+relied+on+the+provision+of+single-layered+descriptions+of+specific+ISAs+to+enable+formal+verification+of+implementations%2C+placing+a+burden+of+correctness+on+these+specifications.+This+work+contributes+by+the+provision+of+a+common+context+for+correct+derivation+of+these+previously+independant+descriptions.+The+work+introduces+novel+levels+of+abstraction+to+allow+re-use+on+any+sequential+computing+machine%2C+provides+a+framework+for+the+comparison+of+different+ISAs+relative+to+a+single+datum%2C+and+enables+analysis+of+design+options+during+the+creation+and+extension+of+ISAs.+Further+contributions+are+the+construction+of+multiple+ISAs+from+a+single+abstract+description%2C+and+the+introduction+of+automatic+source-code+generation+techniques+to+the+Event-B+method%2C+which+include+features+to+assist+in+the+development+and+test+of+useable+ISAs.&rft.date=2009-12-04&rft.type=DEPLOY+Interest+Group+Item&rft.type=NonPeerReviewed&rft.format=application%2Fpdf&rft.identifier=http%3A%2F%2Fdeploy-eprints.ecs.soton.ac.uk%2F163%2F1%2FStephenWrightThesis.pdf&rft.relation=http%3A%2F%2Fwww.cs.bris.ac.uk%2FPublications%2Fpub_master.jsp%3Fid%3D2001121&rft.identifier=++Wright%2C+Stephen++(2009)+PhD+Thesis%3A+Formal+Construction+of+Instruction+Set+Architectures.++%5BDEPLOY+Interest+Group+Item%5D++++(Unpublished)++&rft.relation=http%3A%2F%2Fdeploy-eprints.ecs.soton.ac.uk%2F163%2F<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>