英文翻译.docx

英文翻译.docx

《英文翻译.docx》由会员分享，可在线阅读，更多相关《英文翻译.docx（36页珍藏版）》请在冰点文库上搜索。

英文翻译

ModelCheckingforE-BusinessControlandAssurance

BonnieBrintonAnderson,JamesV.Hansen,PaulBenjaminLowry,

andScottL.Summers

Abstract

Modelcheckingisapromisingtechniquefortheverificationofcomplexsoftwaresystems.AstheuseoftheInternetforconductinge-businessextendsthereachofmanyorganizations,well-designedsoftwarebecomesthefoundationofreliableimplementationofe-businessprocesses.Thesedistributed,electronicmethodsofconductingtransactionsplacerelianceonthecontrolstructuresembeddedinthetransactionprocesses.Deficienciesincontrolstructuresofprocessesthatsupporte-businesscanleadtolossofphysicalassets,digitalassets,money,andconsumerconfidence.Yet,assessingthereliabilityofe-businessprocessesiscomplexand

time-consuming.Thispaperexplicateshowmodel-checkingtechnologycanaidinthedesignandassuranceofe-businessprocessesincomplexdigitalenvironments.Specifically,wedemonstratehowmodelcheckingcanbeusedtoverifye-businessrequirementsconcerningmoneyatomicity,goodsatomicity,validreceipt,andcommunication-linkfailure.Theserequirementsarefundamentaltomanye-businessapplications.

Modelcheckingcanbeusedtotestabroadrangeofsystemsrequirements—notonlyforsystemdesigners,butalsoforauditorsandsecurityspecialists.Systemsthatareexaminedbyauditorsneedtohaveadequatecontrolsbuiltinpriortoimplementationandwillneedadequateauditingafterimplementationtoensurethatnoneoftheprocesseshavebeencorrupted.Modelcheckersmayalsoprovidevalueinexaminingtheprocessesofhighlyintegratedapplicationsasfoundinenterpriseresourceplanningsystems.

IndexTerms：

Atomicity,datatyping,e-Business,modelchecking,processandcommunicationprotocols.

I.INTRODUCTION

Internet-basedbusinessoperationsofferconsiderablepotential,buttheyareaccompaniedbyabroadrangeofoftenunprecedentedrisks.Anactualorperceivedlackofsystemsecurityandreliabilitycansignificantlyconstrainthegrowthofthedigitaleconomy.WhileprogressisbeingmadeinreducingInternetcomputationalrisksthroughavarietyofsoftwarepatchesandcryptographicalgorithms,theseeffortsaddressonlyasmallportionofthelargerchallengeofestablishingthe

necessarysecurityandreliabilityofe-businesssystems.Toresolvethischallenge,systematicmanagementoftheassociatedoperationalrisksisessential[1].

AccordingtoWangetal.[2],managementofoperationalrisksrequirescarefulexaminationofthee-businessinfrastructure.DistributedInternetcomputingischanginge-marketstructuresande-businessmodelsinfundamentalways.Althoughtheflexibilityofdistributede-operationssupportsopenaccessibilityanddynamicinteractions,flexibilitycanintensifyproblemsarisingfrome-marketinformationasymmetryande-businessoperationaluncertainty.Theseproblemsmilitateagainstinnovativee-commercedevelopments.Althoughe-commerceofferstheopportunityforbusinessestogainefficiencyandeffectivenessthroughnetwork-basedad-hocpartnerships,manybusinessesdonottakeadvantageoftheseopportunitiesbecauseoftheheightenedrisksofoperationaluncertaintyandperceivedinformationasymmetryamongunfamiliarbusinesspartners.

ManuscriptreceivedNovember18,2003;revisedMay17,2004.ThispaperwasrecommendedbyAssociateEditorS.Lakshmivarahan.

TheauthorsarewiththeMarriottSchoolofManagementand

KevinandDebraRollinsCenterfore-Business,BrighamYoung

University,Provo,UT84602USA（e-mail:

Bonnie_Anderson@BYU.edu;

James_Hansen@BYU.edu,Paul_Lowry@BYU.edu;Scott_Summers@

BYU.edu）.

DigitalObjectIdentifier10.1109/TSMCC.2004.843181

Theseissuestakeonaddedimportanceasnewbusinessmodelsandarchitectures—suchasInternetauctions,webservices[3]andthesemanticweb[4]—offerbroadsupportforlooselycoupled,e-commercetransactionswherebuyersandsellersmaynothaveanypriortradingexperiencewithoneanother.Forexample,thewebservices[3]platformprovidestheUniversalDescription,DiscoveryandIntegration（UDDI）registryfordiscoveryofe-commerceservices,WSDLforservicedescription,andSOAPfortransactionexecution.Thesefacilitiesrequirenopriorknowledgeofbuyerandsellerbyeitherparty.Insuchenvironments,merchantsandcustomersmaybereluctanttotrustoneanotherandthefollowingsituationsmayarise:

Acustomerisunwillingtopayforaproductwithoutbeingcertainthecorrectproductwillbesent.Amerchantisunwillingtosendaproductwithoutcertaintyofreceivingpayment.Ifamerchantdeliverstheproductwithoutreceivingpayment,afraudulentcustomermayreceivetheproductandthendisappear,witharesultinglosstothemerchant.Ifacustomerpaysbeforereceivingtheproduct,amerchantmaynotdeliverormaydeliverawrongproduct.Thesepossibilitiesunderscoretheneedforcarefullydesignede-commercemodelsthatarerobustunderallevents.

AsWangetal.[5]note,e-systemcomplexityandhumanlimitationsmakeitimpossibletoimagineallscenariosandguaranteecorrectprocessingunderallcircumstances—evenforcarefullydesignedandimplementedcode.Muchofthisdifficultyisduetointerconnectivity,whichwidensthepotentialrangeoferrororvulnerability.Variationinexecutionofconcurrentprocessesinnonstop,nondeterministicsystemsincreasesthepotentialforautomationfailures.Consequentlyminimizingflawsintransactionprotocolsiscrucialforthesurvivalandsustainabilityofe-business.Stakeholders,suchassystemdesigners,users,andauditorsneedmethodstoprecludethesesubtlebutpotentiallycriticalmistakes—beforeerroneousprocessingoccursoranattackerexploitsthem—toenhancecontrolandassurancetoe-commerceusers.Modelcheckingoffersapromisingmethodforaddressingtheseissues.

II.MODELCHECKINGFUNDAMENTALS

Automationfailuresoccurwhenanautomatedsystembehavesdifferentlythanitsstakeholdersexpect.Iftheactualsystembehaviorandthestakeholdersmodelarebothdescribedasfinitestatetransitionsystems,thenmechanizedtechniquesknownasmodelcheckingcanbeusedtoautomaticallydiscoveranyscenariosthatcausethebehaviorsofthetwodescriptionstodivergefromoneanother.Thesescenariosidentifypotentialfailuresandpinpointareaswheredesignchangesorrevisionsshouldbeconsidered

Modelcheckingcantracethroughallrelevantstateswithrespecttoanygivenrequirement.Sincemodelcheckingoperatesonlogicratherthanindividualexecutionpaths,verificationcanbemorethoroughandefficientthantestrunsandsimulation.Someofthemostcompellingfeaturesofmodelcheckersaresummarizedasfollows[6].

1）Theyhelpdelimitasystem’sboundaryortheinterfacebetweenthesystemanditsenvironment.

2）Theypreciselydefineasystem’sdesiredproperties.

3）Theycharacterizeasystem’sbehaviormoreaccurately.Mostcurrentmethodsfocusonfunctionalbehavioronly（e.g.,“Whatisthecorrectanswer?

”）butsomecanhandlereal-timebehavioraswell（e.g.,“Isthecorrectanswerdeliveredontime?

”）.

4）Theycanaidinprovingthatasystemmeetsrequiredspecifications.Byprovidingcounterexamplesthatshowhowspecificationsarenotsatisfied,modelcheckerscanpinpointthecircumstancesunderwhichasystemdoesnotmeetitsspecifications.

Thiscanalsohelptocorrectthesystem.

Thesefeaturesofmodelcheckersaidstakeholdersintwoimportantways.

1）Throughspecification,byfocusingasystemdesigner’sattentiontocrucialquestions,suchas:

Whatistheinterface?

Whataretheassumptionsabouttheapplication’senvironment?

Whatisthesystemsupposedtodounderthisconditionorthatcondition?

Whathappensifthatconditionisnotmet?

Whatarethesystem’sinvariantproperties?

2）Throughverification,byprovidingadditionalassurance.Relyingonproofthatasystemmeetsitssecuritygoalsisbetterthanrelyingonopinion—evenexpertopinion.

Itshouldbeemphasizedthatanyproofofcorrectnessisrelativetoboththeformalspecificationofasystemandtheformalspecificationofthedesiredproperties:

asystemprovencorrectwithrespecttoanincorrectspecificationleavesnoassuranceaboutthesystematall.

Theprocessofprovingentailsthreeactions:

First,thesystemofinterestmustbemodeled.Amathematicalmodelisconstructedthatexpressesthesemanticstructureofane-businessimplementation.

Second,allpropertiestobeguaranteedintheimplementationareformallyspecified.Inane-businesscontext,onesuchspecificationmightbethatgoodsmustalwaysbereceivedbeforepaymentisinitiated.

Third,aproofisprovided.Typically,aproofreliesoninductionovertracesofthee-commercecommunicationandtransactionoperations.

Ingeneral,verifyingthatanye-businessprocessisresilienttohiddenflawsanderrorsisadauntingtask.Manualmethodsareslowanderrorprone.Eventheoremprovers,whichprovideaformalstructureforverifyingstandardcharacteristics,mayrequirehumaninterventionandcanbetime-consuming.Moreover,evenifafailureisfoundusingatheoremprover,itmayprovidelittlehelpinlocatingthesourceofthe

failure[2].Simulationsoffercomputationalpower,buttheyareadhocinnatureandthereisnoguaranteetheywillexploreallimportantcontingencies[2].

Incontrast,modelcheckingisanevolvingtechnologythatcanprovideeffectiveandefficientevaluationofe-businessprocesses.Modelcheckingwasoriginallydevelopedforvalidatinghighlycomplexintegratedcircuitsandsoftwarepackages[7],[8],butithasrecentlybeenadoptedtotacklethecomplexityofe-commercetransactions[9],

[2],[10].Currentmodel-checkingtechnologyisbasedonautomatedtechniquesthata