[發(fā)明專(zhuān)利]一種基于參數(shù)化模型的Web服務(wù)組合驗(yàn)證方法

有效

• 申請(qǐng)?zhí)枺?/td>: 201711420311.3
• 申請(qǐng)日: 2017-12-25
• 公開(kāi)（公告）號(hào): CN108170404B
• 公開(kāi)（公告）日: 2021-04-06
• 發(fā)明（設(shè)計(jì)）人: 周宇;周世旗;周女琪
• 申請(qǐng)（專(zhuān)利權(quán)）人: 南京航空航天大學(xué)
• 主分類(lèi)號(hào): G06F8/10
• 分類(lèi)號(hào): G06F8/10;G06F8/20
• 代理公司: 江蘇圣典律師事務(wù)所 32237
• 代理人: 賀翔

本發(fā)明公開(kāi)了一種基于參數(shù)化模型的Web服務(wù)組合驗(yàn)證方法，包括：抽象出Web服務(wù)組合過(guò)程與QoS屬性，確定QoS屬性的組成部分；分析影響QoS屬性的環(huán)境條件，并將該環(huán)境條件建模為參數(shù)化的馬爾可夫決策過(guò)程；引入限制要求約束Web服務(wù)組合過(guò)程，并將該過(guò)程建模成為帶限制要求的參數(shù)化馬爾可夫決策過(guò)程；將待驗(yàn)證的QoS屬性建模成為時(shí)序邏輯公式；使用可處理參數(shù)化模型的概率模型檢測(cè)工具，驗(yàn)證有窮狀態(tài)模型在動(dòng)態(tài)的環(huán)境下是否滿(mǎn)足待驗(yàn)證的QoS屬性，并得到定量驗(yàn)證結(jié)果。本發(fā)明方法解決了在復(fù)雜的開(kāi)放環(huán)境下，由于環(huán)境動(dòng)態(tài)變化的隨機(jī)性、抽象服務(wù)之間的依賴(lài)性所導(dǎo)致的傳統(tǒng)Web服務(wù)組合驗(yàn)證方法不準(zhǔn)確的問(wèn)題，并有效地緩解了驗(yàn)證過(guò)程中的狀態(tài)爆炸問(wèn)題。

技術(shù)領(lǐng)域

本發(fā)明屬于計(jì)算機(jī)軟件工程開(kāi)發(fā)技術(shù)領(lǐng)域，特別涉及一種基于參數(shù)化模型的Web服務(wù)組合驗(yàn)證方法。

背景技術(shù)

Web服務(wù)組合是將不同的具體服務(wù)組合起來(lái)以完成功能更強(qiáng)大的組合服務(wù)的技術(shù)。隨著Web服務(wù)技術(shù)的快速發(fā)展，功能屬性類(lèi)似而服務(wù)質(zhì)量(Quality of Service，即QoS)不同的具體服務(wù)數(shù)量急速增加。在此情況下，根據(jù)服務(wù)質(zhì)量為用戶(hù)推薦不同的具體服務(wù)以使得整個(gè)Web服務(wù)組合的全局QoS值最優(yōu)的方法稱(chēng)之為QoS感知的Web服務(wù)組合方法。另外，環(huán)境是動(dòng)態(tài)變化的，當(dāng)環(huán)境變化時(shí)具體服務(wù)的QoS值也會(huì)隨之變化。因此，如何在動(dòng)態(tài)變化的環(huán)境中選擇服務(wù)使得全局QoS最優(yōu)，是開(kāi)放環(huán)境下QoS感知的Web服務(wù)組合研究中的重要問(wèn)題。

概率模型檢測(cè)技術(shù)作為一種形式化驗(yàn)證方法，其目的在于使用有窮狀態(tài)模型描述給定的概率系統(tǒng)，使用時(shí)序邏輯公式描述待驗(yàn)證的屬性，并將有窮狀態(tài)模型與時(shí)序邏輯公式作為模型檢測(cè)工具的輸入，驗(yàn)證概率系統(tǒng)是否滿(mǎn)足待驗(yàn)證的屬性，并給出定量結(jié)果。PRISM作為一款被廣泛使用的概率模型檢測(cè)工具，可用于分析具有概率行為和隨機(jī)性行為的系統(tǒng)并進(jìn)行相關(guān)屬性驗(yàn)證。以上將概率模型檢測(cè)技術(shù)應(yīng)用于Web服務(wù)組合研究的相關(guān)方法稱(chēng)為Web服務(wù)組合驗(yàn)證方法。

PARAM是本方法中用到的工具，它是一款可以處理參數(shù)化模型的概率模型檢測(cè)工具，是PRISM的拓展。PARAM與PRISM的區(qū)別在于，PARAM可以處理參數(shù)化模型。所以，與PRISM一樣，PARAM是一個(gè)用來(lái)分析概率系統(tǒng)的工具，可以支持三種類(lèi)型的模型，離散時(shí)間馬爾可夫鏈，連續(xù)時(shí)間的馬爾可夫鏈以及馬爾可夫決策過(guò)程。該工具通過(guò)自動(dòng)分析建立好的參數(shù)化模型與時(shí)序邏輯公式，將得到含有多個(gè)變量的有理函數(shù)，這些變量就是在建模過(guò)程中被參數(shù)化的變量。根據(jù)定義域給定該變量的值，并帶入有理函數(shù)計(jì)算，就可求出待驗(yàn)證的屬性的定量分析結(jié)果。

對(duì)于開(kāi)放環(huán)境下的Web服務(wù)組合過(guò)程來(lái)說(shuō)，首先，環(huán)境的動(dòng)態(tài)變化將會(huì)影響不同具體服務(wù)的QoS值，從而影響到Web服務(wù)的選擇。而環(huán)境的動(dòng)態(tài)變化是隨機(jī)的，使用參數(shù)化的馬爾可夫決策過(guò)程對(duì)環(huán)境的動(dòng)態(tài)變化進(jìn)行建模，可以真實(shí)模擬環(huán)境的動(dòng)態(tài)變化，從而提高開(kāi)放環(huán)境下Web服務(wù)組合驗(yàn)證方法的準(zhǔn)確性。其次，在實(shí)際的Web服務(wù)組合場(chǎng)景中，抽象服務(wù)之間不是相互獨(dú)立的，不同服務(wù)之間可能存在相互依賴(lài)的情況。為解決這個(gè)問(wèn)題，本發(fā)明引入限制要求來(lái)約束Web服務(wù)組合過(guò)程，同時(shí)也可以緩解驗(yàn)證過(guò)程中的狀態(tài)爆炸問(wèn)題。最后，使環(huán)境條件的參數(shù)化馬爾可夫決策過(guò)程與Web服務(wù)組合過(guò)程的帶限制要求的參數(shù)化馬爾可夫決策過(guò)程相交互并作為PARAM一個(gè)輸入，待驗(yàn)證的QoS屬性的時(shí)序邏輯公式作為另一個(gè)輸入。使用PARAM驗(yàn)證，便可得到帶有變量的有理函數(shù)。給定變量的具體值后，就能得到時(shí)序邏輯公式的驗(yàn)證結(jié)果，即可得到與結(jié)果相應(yīng)的狀態(tài)轉(zhuǎn)換路徑，也就是最優(yōu)的Web服務(wù)組合方式。因此，使用PARAM對(duì)Web服務(wù)組合過(guò)程進(jìn)行驗(yàn)證，可以解決開(kāi)放環(huán)境下QoS感知的Web服務(wù)組合研究中的相關(guān)問(wèn)題。

之前對(duì)QoS感知的Web服務(wù)組合驗(yàn)證方法的研究集中于用戶(hù)的非功能屬性的多目標(biāo)性與不確定性的處理，并未考慮到環(huán)境動(dòng)態(tài)變化的隨機(jī)性對(duì)Web服務(wù)組合過(guò)程的影響。同時(shí)，也很少考慮到實(shí)際情況下抽象服務(wù)之間相互依賴(lài)所帶來(lái)的Web服務(wù)組合方法不準(zhǔn)確的問(wèn)題。

發(fā)明內(nèi)容