基于謂詞抽象與精化技術的web服務驗證研究

1、蘇州大學碩士學位論文基于謂詞抽象與精華技術的Web服務驗證研究姓名：任強申請學位級別：碩士專業(yè)：計算機軟件與理論指導教師：張廣泉201105ResearchonVerificationofWebServiceBasedonAbstractionRefinementandCombinationTechnologyAbstractServiceorientedarchitecture(SOA)isanewsoftwaredevelopmen

2、t，deploymentandintegratedmodelaftertheobjectoriented，componentbaseddevelopment，andprovidesflexibledesignanddevelopmentprogramsforsoftwaredevelopmentAsamethodofSOA，Webservicesbreakthroughthetraditionaldistributedcomputing

3、modelincommunication，applicationrangeandotherconstraintsAndthroughthewayofservicescombination，thenetworkapplicationthatconstructsflexiblyandrapidlyhaspenetratedintomanyofthekeyindustriesofnationaleconomyIntheexistingveri

4、ficationmethodsofWebservices，modelcheckinghasbeenwidelyusedbecauseithashi曲degreeofautomation，andCallprovideacounterexamplepathHowever，becauseofthelargescaleofthesystem，themodelcheckingwillcausethestatespaceexplosionprobl

5、emintheprocess，howtoselectthesuitablewaytorelievestatespaceexplosionhasbecomearesearchhotspotinserviceverificationfieldInthisdissertation，byintroducingpredicateabstractionandrefinementtechniquesintothetraditionalmodelche

6、ckingmethod，weproposeanabstractionrefinementverificationframeworkforWebservices，toverifythesecurityoftheinternalprocesslogicandthecompatibilitybetweenservicesMajorworkandcontributionsofthisdissertationareasfollows：First，

7、weUseKripkestructuretOconstructthemodelforWebservice，andgainpredicateformulacollectionthroughdisintegratingpropertiesintoatomproposition，thencomposetheabstractKripkestructureusingpredicateabstracttechniques，andfinallycom

8、bineallabstractmodelstOgetthecombinedabstractmodelofverificationsystemSecond，weproposetheruleofconversionabstractKripkestructuretoPromelalanguage，thenverifythepropertieswiththeSpinmodelchecker，ifnotsatisfied，thecounterex