本文關(guān)鍵詞：基于VerICS的Web服務(wù)建模與驗證

  更多相關(guān)文章： Web服務(wù)組合 模型檢測 BPEL VerICS 時態(tài)認(rèn)知邏輯

【摘要】：SOA的出現(xiàn)和快速發(fā)展,使得Web服務(wù)在軟件開發(fā)過程中成為了一個舉足輕重的角色。由于單一Web服務(wù)功能受限,它們很難滿足用戶日益復(fù)雜的需求,很多情況下需要將已存的原子Web服務(wù)組合起來以實現(xiàn)目標(biāo)需求。然而,受到服務(wù)本身的特性、復(fù)雜多變的網(wǎng)絡(luò)運行環(huán)境及服務(wù)開發(fā)模式的影響,服務(wù)組合的正確性、安全性、時效性性等可信性質(zhì)很容易受到威脅,為保證Web服務(wù)組合的正確運行,有必要對Web服務(wù)組合進(jìn)行可信性質(zhì)的驗證工作。形式化方法中的模型檢測技術(shù)通常被用來建模Web服務(wù)組合的運行過程以及驗證Web服務(wù)組合的可信性質(zhì)。針對傳統(tǒng)的模型檢測方法并不能驗證帶有時間約束的Web服務(wù)組合相關(guān)性質(zhì)的缺陷,本文提出了一種基于VerICS的Web服務(wù)建模與驗證方法,該方法不僅能夠驗證帶有時間約束的Web服務(wù)組合的時態(tài)邏輯性質(zhì),還能夠驗證Web服務(wù)組合的認(rèn)知邏輯性質(zhì)。本文的工作分為以下幾個方面:(1)為了能夠使用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的輸入語言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)認(rèn)知邏輯性質(zhì)進(jìn)行驗證,根據(jù)驗證結(jié)果判定該Web服務(wù)組合是否滿足目標(biāo)需求。這個實例說明了本文所提出的針對Web服務(wù)組合建模與驗證的方法的可行性及有效性。
【關(guān)鍵詞】：Web服務(wù)組合 模型檢測 BPEL VerICS 時態(tài)認(rèn)知邏輯
【學(xué)位授予單位】：華僑大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2016
【分類號】：TP393.09
【目錄】：

• 摘要3-5
• Abstract5-9
• 第1章 緒論9-16
• 1.1 研究背景及意義9-10
• 1.2 國內(nèi)外研究現(xiàn)狀10-13
• 1.2.1 Petri網(wǎng)方法10-11
• 1.2.2 進(jìn)程代數(shù)方法11
• 1.2.3 有限狀態(tài)機方法11-12
• 1.2.4 時態(tài)認(rèn)知邏輯模型檢測方法12-13
• 1.3 本文研究內(nèi)容與創(chuàng)新點13-14
• 1.4 論文結(jié)構(gòu)14-16
• 第2章 模型檢測16-25
• 2.1 Kripke結(jié)構(gòu)16-17
• 2.2 時態(tài)邏輯17-19
• 2.2.1 線性時態(tài)邏輯LTL17-18
• 2.2.2 計算樹邏輯CTL*18-19
• 2.3 知識推理19-21
• 2.4 時態(tài)認(rèn)知邏輯CTLKD21-23
• 2.5 模型檢測工具VerICS23-24
• 2.6 本章小結(jié)24-25
• 第3章 Web服務(wù)業(yè)務(wù)流程25-29
• 3.1 Web服務(wù)及其體系結(jié)構(gòu)25-26
• 3.1.1 Web服務(wù)定義25
• 3.1.2 Web服務(wù)體系結(jié)構(gòu)25-26
• 3.2 Web服務(wù)組合26-27
• 3.3 Web服務(wù)業(yè)務(wù)流程執(zhí)行語言BPEL27-28
• 3.3.1 BPEL定義27
• 3.3.2 BPEL組成27
• 3.3.3 BPEL活動介紹27-28
• 3.4 本章小結(jié)28-29
• 第4章 BPEL形式模型及其自動化模型檢測方法29-65
• 4.1 BPEL時間約束屬性的擴展29-31
• 4.2 BPEL形式模型BIOSTS31-32
• 4.3 BPEL活動形式化建模32-50
• 4.3.1 BEPL基本活動形式化建模32-41
• 4.3.2 BPEL結(jié)構(gòu)活動形式化建模41-50
• 4.4 BPEL流程自動化模型檢測方法50-60
• 4.4.1 BPEL到BIOSTS轉(zhuǎn)化算法50-55
• 4.4.2 BIOSTS到IL轉(zhuǎn)化算法55-60
• 4.5 Web服務(wù)組合建模與驗證框架60-64
• 4.5.1 時態(tài)認(rèn)知邏輯ECTLKD與TECTLK61-62
• 4.5.2 框架結(jié)構(gòu)62-64
• 4.6 本章小結(jié)64-65
• 第5章 實例研究65-76
• 5.1 VTA概述65
• 5.2 BPEL時間約束屬性擴展65-67
• 5.3 將 BPEL 轉(zhuǎn)化為 BIOSTS67-69
• 5.4 將BIOSTS轉(zhuǎn)化為IL69-73
• 5.5 VTA規(guī)范驗證73-75
• 5.6 本章小結(jié)75-76
• 第6章 總結(jié)與展望76-78
• 參考文獻(xiàn)78-83
• 致謝83-84
• 個人簡歷、在學(xué)期間發(fā)表的學(xué)術(shù)論文及研究成果84

，

本文編號：734631