面向服務(wù)的多參與者協(xié)調(diào)建模驗證.pdf

1、南京航空航天大學(xué)碩士學(xué)位論文面向服務(wù)的多參與者協(xié)調(diào)建模驗證姓名：閆艷申請學(xué)位級別：碩士專業(yè)：計算機科學(xué)與技術(shù)指導(dǎo)教師：黃志球201012面向服務(wù)的多參與者協(xié)調(diào)建模驗證IIAbstractThereliabilityofWebservicesneedstransaction.DuetosomeacteristicsofWebservicessuchasautonomyflexibilityheterogeneoussoonthetradi

2、tionaltransactionsemanticsprotocolshaveproventobeinappropriate.AsWebServicesTransactionstardWSTransaction(WSTx)specificationsdefinemechanismsftransactionalinteroperabilitybetweenWebservicesdomainsprovideameanstocomposetr

3、ansactionalqualitiesofserviceintoWebservicesapplications.WSTxillustratestheabstractbehavioftheprotocolbetweenacodinataparticipantthroughtheabstractstatediagramwithoutgivingthespecificstrategyfacodinatwithmultipleparticip

4、ants.NowadaysdescribingverfyingWebservicescompositiontransactionisanimptantresearchdirectionbutcurrentresearchmainlyrevolvesaroundthemodelingoftransactionprotocolsrarelyfocusesonthebehaviofcodination.Sointhisthesisanappr

5、oachofmodelingverifyingserviceientedmultiparticipantscodinationisproposedthemainresearchwkscanbelistedasfollows.FirstofallthemultiparticipantscodinationmodelofWebservicesbasedonWSTxprotocolisproposedwhichdividesthedepend

6、encyrelationsbetweenparticipantsinto:DominantDependentConcurrentExclusion.AccdingtoeachrelationthespecificcodinationstrategyisgivenSecondlyconsideringthefmalmethodPicalculusisadoptedthemappingtablemodelingrulesfromWebser

7、vicescodinationelementstoPicalculussyntaxaregiveninthisdissertation.OnthebasisofmappingtablebetweenthecodinationelementsPicalculuselemesthepicalculusmodelofBPELprocesscanbeobtainedwithalgithmdeionAftermodelingofmultipart

8、icipantscodinationsafetylivenessaredefinedrespectivelyinthecodinationintermsofthedependencyrelationsbetweentheparticipantswhicharethenrepresentedinCTL(ComputationTreeLogic).FinallyaframewkfverificationofPicalculusbasedon