?url_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Adc&rft.title=Formal+Modelling+and+Analysis+of+Business+Information%0D%0AApplications+with+Fault+Tolerant+Middleware+%0D%0A%0D%0A&rft.creator=Bryans%2C+Jeremy+W.&rft.creator=Fitzgerald%2C+John+S.&rft.creator=Alexander%2C+Romanovsky&rft.creator=Andreas%2C+Roth&rft.subject=Composition+and+reuse&rft.subject=Business&rft.subject=Resilience&rft.subject=Event-B+Examples&rft.description=Distributed+information+systems+are+critical+to+the+functioning+of%0D%0Amany+businesses%3B+designing+them+to+be+dependable+is+a+challenging+but%0D%0Aimportant+task.+We+report+our+experience+in+using+formal+methods+to%0D%0Aenhance+processes+and+tools+for+development+of+business+information%0D%0Asoftware+based+on+service-oriented+architectures.+In+our+work%2C+which%0D%0Atakes+place+in+an+industrial+setting%2C+we+focus+on+the+configuration+of%0D%0Amiddleware%2C+verifying+application-level+requirements+in+the+presence%0D%0Aof+faults.+In+pilot+studies+provided+by+SAP%2C+we+used+the+Event-B%0D%0Aformalism+and+the+open+RODIN+tools+platform+to+prove+properties+of%0D%0Amodels+of+business+protocols+and+expose+weaknesses+of+certain%0D%0Amiddleware+configurations+with+respect+to+particular+protocols.+We%0D%0Athen+extended+the+approach+to+use+models+automatically+generated+from%0D%0Adiagrammatic+design+tools%2C+opening+the+possibility+of+seamless%0D%0Aintegration+with+current+development+environments.+Increased%0D%0Aautomation+in+the+verification+process%2C+through+domain-specific+models%0D%0Aand+theories%2C+is+a+goal+for+future+work.+++&rft.publisher=Newcastle+University&rft.date=2008-12-15&rft.type=Other&rft.type=NonPeerReviewed&rft.format=application%2Fpdf&rft.identifier=http%3A%2F%2Fdeploy-eprints.ecs.soton.ac.uk%2F52%2F1%2FBryans-et-al.pdf&rft.relation=http%3A%2F%2Fwww.cs.ncl.ac.uk%2Fpublications%2Ftechreports%2Ftrs%2Fpapers%2F1131.pdf&rft.identifier=++Bryans%2C+Jeremy+W.+and+Fitzgerald%2C+John+S.+and+Alexander%2C+Romanovsky+and+Andreas%2C+Roth++(2008)+Formal+Modelling+and+Analysis+of+Business+Information+Applications+with+Fault+Tolerant+Middleware.++Newcastle+University%2C+Newcastle+University+TR%2C+accepted+to+appear+in+Proceedings+of+ICECCS+2009.++++(In+Press)++&rft.relation=http%3A%2F%2Fdeploy-eprints.ecs.soton.ac.uk%2F52%2F<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>