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

1、南京航空航天大學碩士學位論文面向服務的多參與者協(xié)調(diào)建模驗證姓名：閆艷申請學位級別：碩士專業(yè)：計算機科學與技術指導教師：黃志球201012面向服務的多參與者協(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