一種Web服務(wù)組合的認(rèn)知模型檢測方法.pdf

1、由于 Web服務(wù)及其協(xié)同的動(dòng)態(tài)性、開放多變的互聯(lián)網(wǎng)運(yùn)行環(huán)境以及松耦合的服務(wù)開發(fā)模式,所導(dǎo)致的開發(fā)和運(yùn)行過程的不確定性,使得 Web服務(wù)組合的正確性和可靠性等可信性質(zhì)難以得到保證。因此,形式化分析和驗(yàn)證 Web服務(wù)組合的研究也越來越受到重視。當(dāng)前針對 Web服務(wù)的模型檢測方法和工具還比較少,建模與驗(yàn)證環(huán)節(jié)均需手工處理,因此驗(yàn)證過程自動(dòng)化程度較低;另外,Web服務(wù)組合可視為一種典型的多智能體系統(tǒng),因此驗(yàn)證多智能體系統(tǒng)特有的知識(shí)與合作等性質(zhì)也

2、具有重要意義。
　　為了提高Web服務(wù)組合的形式化建模的自動(dòng)化程度,支持對知識(shí)、合作等Web服務(wù)認(rèn)知狀態(tài)及其時(shí)態(tài)演變等性質(zhì)的驗(yàn)證,本文以多智能體系統(tǒng)模型檢測工具M(jìn)CMAS底層驗(yàn)證平臺(tái),設(shè)計(jì)并實(shí)現(xiàn)了Web服務(wù)組合的自動(dòng)驗(yàn)證原型系統(tǒng)MCWS。首先,用BPEL狀態(tài)遷移系統(tǒng)對業(yè)務(wù)流程執(zhí)行語言BPEL進(jìn)行形式化建模,給出基本活動(dòng)、結(jié)構(gòu)化活動(dòng)、錯(cuò)誤處理和補(bǔ)償處理的的形式語義;然后,提出自動(dòng)驗(yàn)證 Web服務(wù)組合的MCWS系統(tǒng)架構(gòu),設(shè)計(jì)并實(shí)現(xiàn)了B