基于verics的web服務(wù)建模與驗證

《基于verics的web服務(wù)建模與驗證》由會員上傳分享，免費在線閱讀，更多相關(guān)內(nèi)容在學(xué)術(shù)論文-天天文庫。

1、學(xué)校代碼：10385分類號：研究生學(xué)號：1300220006密級：基于VerICS的Web服務(wù)建模與驗證AModelingandVerificationMethodforWebServicesBasedonVerICS作者姓名：杜萬蕭指導(dǎo)教師：駱翔宇副教授學(xué)科：計算機科學(xué)與技術(shù)研究方向：形式化方法所在學(xué)院：計算機科學(xué)與技術(shù)學(xué)院論文提交日期：二零一六年六月一日學(xué)位論文獨創(chuàng)性聲明本人聲明茲呈交的學(xué)位論文是本人在導(dǎo)師指導(dǎo)下完成的研究成果。論文寫作中不包含其他人己經(jīng)發(fā)表或撰寫過的研究內(nèi)容，如參考。他人或集體的科研成果，均在論文中Ｌ乂明確的方式說明本人依法享有和承擔(dān)由此論文所產(chǎn)生的權(quán)利和

2、責(zé)任。日占、了，：論文作者簽名：幸茍簽名期學(xué)位論文版權(quán)使用授權(quán)聲明本人同意授權(quán)華僑大學(xué)有權(quán)保留并向國家機關(guān)或機構(gòu)送交學(xué)位論文的復(fù)印件和電子肢，允許學(xué)位論文被查閱和借閱。本人授權(quán)華僑大學(xué)可Ｌ義將本學(xué)位論文的全部內(nèi)容或部分內(nèi)容編入有關(guān)數(shù)據(jù)庫進行檢索ｋ乂采用影印、縮印或擔(dān)描等復(fù)制手段保存和匯編本學(xué)位論文。，可：論文作者簽名：和哨指導(dǎo)教師簽華換轉(zhuǎn)］．．日期簽名日期簽名：從摘要摘要SOA的出現(xiàn)和快速發(fā)展，使得Web服務(wù)在軟件開發(fā)過程中成為了一個舉足輕重的角色。由于單一Web服務(wù)功能受限，它們很難滿足用戶日益復(fù)雜的需求，很多情況下需要將已存的原子Web服務(wù)組合起來以實

3、現(xiàn)目標(biāo)需求。然而，受到服務(wù)本身的特性、復(fù)雜多變的網(wǎng)絡(luò)運行環(huán)境及服務(wù)開發(fā)模式的影響，服務(wù)組合的正確性、安全性、時效性性等可信性質(zhì)很容易受到威脅，為保證Web服務(wù)組合的正確運行，有必要對Web服務(wù)組合進行可信性質(zhì)的驗證工作。形式化方法中的模型檢測技術(shù)通常被用來建模Web服務(wù)組合的運行過程以及驗證Web服務(wù)組合的可信性質(zhì)。針對傳統(tǒng)的模型檢測方法并不能驗證帶有時間約束的Web服務(wù)組合相關(guān)性質(zhì)的缺陷，本文提出了一種基于VerICS的Web服務(wù)建模與驗證方法，該方法不僅能夠驗證帶有時間約束的Web服務(wù)組合的時態(tài)邏輯性質(zhì)，還能夠驗證Web服務(wù)組合的認知邏輯性質(zhì)。本文的工作分為以下幾個方面：（1）為了能夠使用

4、VerICS驗證帶有時間約束屬性的Web服務(wù)組合的相關(guān)性質(zhì)，首先提出了Web服務(wù)業(yè)務(wù)流程描述語言BPEL的時間約束屬性擴展方法；（2）提出BPEL流程與VerICS輸入語言IL的“中間橋梁”BPEL輸入輸出狀態(tài)遷移系統(tǒng)BIOSTS形式模型的概念，給出BPEL流程各基本活動與結(jié)構(gòu)活動的的BIOSTS形式化建模過程，為下一步提供BPEL流程的自動化驗證程度打下基礎(chǔ)；（3）提出BPEL流程到BIOSTS的轉(zhuǎn)化算法BP2BS，以及BPEL各結(jié)構(gòu)活動到BIOSTS的轉(zhuǎn)化算法。這一系列算法實現(xiàn)了BPEL流程的自動形式化建模，提高了Web服務(wù)組合的自動化驗證程度；（4）提出BIOSTS到VerICS的輸入語

5、言IL的轉(zhuǎn)化算法BS2IL。該算法綜合考慮形式模型BIOSTS的特征與IL的語法特征，將BIOSTS包含的各元素轉(zhuǎn)化為IL語言中的各個組成部分；實現(xiàn)了二者之間的自動轉(zhuǎn)化，減少轉(zhuǎn)化過程中繁瑣的人工編碼工作，實現(xiàn)BPEL流程的自動化模型檢測；（5）運用模型檢測工具VerICS對虛擬旅游系統(tǒng)VTA的時態(tài)認知邏輯性質(zhì)I華僑大學(xué)碩士學(xué)位論文進行驗證，根據(jù)驗證結(jié)果判定該Web服務(wù)組合是否滿足目標(biāo)需求。這個實例說明了本文所提出的針對Web服務(wù)組合建模與驗證的方法的可行性及有效性。關(guān)鍵詞：Web服務(wù)組合模型檢測BPELVerICS時態(tài)認知邏輯IIAbstractAbstractTheemergenceandr

6、apiddevelopmentofservice-orientedarchitecturemakestheWebservicebecomingaveryimportantroleintheprocessofsoftwaredevelopment.AsingleWebservicecan'tsatisfyincreasinglycomplexrequirementsofusersbecauseofit'slimitedfunctions.Inmostsituations,weneedtocombinetheexistingsingleWebservicestoachieveourtargetre

7、quirements.However,thecredibilityofWebservicecompositionwhichincludescorrectness,security,reliabilityandsoon,isthreatenedeasilybecauseofthecharacteristicsoftheserviceitself,openandvolatileoperatingdev