Web服務(wù)組合建模和驗證技術(shù)研究.pdf

1、東南大學(xué)博士學(xué)位論文Web服務(wù)組合建模和驗證技術(shù)研究姓名：張鵬程申請學(xué)位級別：博士專業(yè)：計算機(jī)軟件與理論指導(dǎo)教師：李必信徐寶文20091201東南大學(xué)博士學(xué)位論文AbstractSOA(ServiceOrientedArchitecture)isthemostpromisingtrendofdistributedcomputingandsoftwaredevelopmentThegoalofSOAistoefficientlysolve

2、thedistributedapplicationintegrationbasedonW|ebservicesindistributeddynamicandheterogeneousenvironmentsWebservicesa他autonomousplatformindependentnetworkcomponentsthathavesomenewattributessuch勰loosecouplingdynamiccomposit

3、ionreconfigurationprovidinganewtechniquefordistributedapplicationandsoftwaredevelopmentonIntemetSomeservicesaredynamicallycomposedtoformanewcompositeserviceforsatisfyingusers’requirementsnecompositionprocessisdescribedby

4、WebservicecompositiondescriptionlanguagessuchasWS—BPEL(WebServiceBusinessProcessExecutionLanguage)andWSCDL(WebServicesChoreographyDescriptionLanguage)However，theselanguageshavetwomainproblemsOntheonehandtheselanguagesare

5、basedonXML，andlackthetheoreticalfoundationofmodelingOntheotherbandtheselanguagescannotprovideanymeanstoverifythecorrectnessofspecificationInordertosolvetheseproblems，thedissertationsystematicallyinvestigatesthemodelingst

6、aticanddynamicverificationofWebservicecompositionNotonlythecorrectuessofspecificationneedstobeverifiedatdesigntime，butalsodynamicverificationtechniqueisusedfortheassuranceofcorrectnessofspecificationatruntimeTherefore，th

7、emaincontributioilsofthedissertationarelisted私follows：FirstweproposeamodelingapproachofWSCDLbasedonUMLmodelsWe蹴UMLComponentDiagramstorepresentthestructuralmodelofWSCDLActivitymodelamongeachroleinWSCDLismodeledbyUMLSequen

8、ceDiagrams，thenIYMLStatemachinemodelsrepresentingbehaviormodelofsingleroleareautomaticallygeneratedfromUMLSequencediagramsDataflowisobtainedfromWSDLspecificationandthenispresentedbyUMLClassdiagrams111eapproachprovidesagr

9、aphicalfrontendfordesignerstodirectlydesignWebservicecompositionmodel111edataflowinwebservicecompositionprocessisalsoconsideredSecondweproposeamodelcheckingapproachofWSCDLbasedonUMLmodelatdesigntime1f11eUMLmodelsaretrans

10、latedintotheinputlanguageofCadenceSMVmodelcheckerforverifyingwhetherU～幾modelssatisfydesiredpropertiesTheapproachcannotonlycanverifystructuralandbehavioralproperties，butalsocanverifydatapropertiesinWSCDL11地experimentsshow

11、theapproachcanverifysomecriticalpropertiesinamiddle—scaledataenrichedWebservicecompositionThirdweproposeanapproachformonitoringoftemporalpropertiesincompositeservicebasedonPSC砒runtimeAnovelscenariobasednotationPSC(Proper

12、tySequenceChart)isintroducedTheformalsyntaxandsemanticsofPSCaredefinedWethenuseruntimemonitoringtechniquetocontinuouslydetectwhethertheexecutiontracesofwebservicecompositionareconsistentwithtemporalpropertiesspecifiedbyP

13、SCn屺experimentsshowthattheapproachcanefficientlydetecttheerrorsincompositeserviceatruntimeMoreovertemporalpropertiesrepresentedbyPSCaresimpleandeasilyunderstoodwhichaddressestheproblemthatpropertiesrepresentedbytemporall

14、ogicsarenotintuitiveandclearForthweproposeallapproachformonitoringoftimedpropertiesincompositeservicebasedonTPSCatruntimeConsideringthegraphicalattributeofPSC，PSCisextendedintoTPSC(TunedPSC)tepresenttimedproperties11塢sem

15、anticsofTPSCisgivenbasedontimedBUchiautomatonandtheexpressivenessofTPSCismeasuredbasedonrealtimespecificationpatternWethen峨runtimemonitoringtechniquetocontinuouslydetectwhethertheactualbehaviorofwebservicecompositionproc

16、esssatisfiestheexpectedtimedproperties1f1艙approachoanalsocountwhethertheprobabilityforatimedpropertyholdsatruntimeneframeworkhasbeenappliedtoacasestudyandaseriesofexperimentshavebeenreportedthatvalidatetheperformanceofth