基于時態(tài)認(rèn)知邏輯的Web服務(wù)模型檢測.pdf

1、互聯(lián)網(wǎng)的開放性使得Web服務(wù)是分布式的,在Web服務(wù)交互過程中,一些“不正?！钡南⒔换绊慦eb服務(wù)的質(zhì)量和健壯性,降低用戶滿意度,甚至破壞正常的服務(wù)過程,因此,驗證Web服務(wù)的安全性和可靠性很有必要。模型檢測技術(shù)由于其自動化程度高,已經(jīng)在Web服務(wù)的形式化驗證中得到了成功的應(yīng)用,模型檢測技術(shù)是很好的驗證Web服務(wù)可靠性和安全性的方法。傳統(tǒng)模型檢測技術(shù)主要采用時態(tài)邏輯描述被驗證的規(guī)范,人們較少注意認(rèn)知邏輯的模型檢測問題。因而傳統(tǒng)模型

2、檢測技術(shù)不能檢測知識的相關(guān)屬性,也不能有效的保證系統(tǒng)的可靠性和安全性;而時態(tài)認(rèn)知邏輯模型檢測技術(shù)可以很好的驗證知識屬性,并更好的保證系統(tǒng)的可靠性和安全性。因此,論文采用時態(tài)認(rèn)知邏輯的模型檢驗技術(shù)來驗證Web服務(wù)這一當(dāng)前的研究熱點問題。
　　本文用時態(tài)認(rèn)知邏輯模型檢測技術(shù)對Web服務(wù)組合問題和特征交互問題進(jìn)行了形式化驗證。據(jù)我們所知,目前,國內(nèi)外還沒有用時態(tài)認(rèn)知邏輯模型檢測技術(shù)對Web服務(wù)的特征交互問題進(jìn)行驗證的相關(guān)報道。論文提出了

3、從Web服務(wù)的描述語言BPEL到本文的模型檢測工具(MCTK)的形式化驗證框架,給出了從Web服務(wù)的過程描述模型(BPEL)到形式化模型(有限狀態(tài)機模型)的轉(zhuǎn)換框架,這將使得Web服務(wù)的形式化驗證工作更加自動化。并且本論文把時態(tài)認(rèn)知邏輯模型檢測技術(shù)擴展應(yīng)用到了安全領(lǐng)域,對安全協(xié)議進(jìn)行了形式化驗證,并發(fā)現(xiàn)了其中的漏洞。本文取得的一些研究成果如下:
　　(1)提出了用時態(tài)認(rèn)知邏輯模型檢測技術(shù)對Web服務(wù)組合問題進(jìn)行形式化驗證的方法。用

4、本文的時態(tài)認(rèn)知邏輯模型檢測工具M(jìn)CTK對Web服務(wù)的組合問題進(jìn)行了分析和驗證,分析了Web服務(wù)流程的正確性,并且能夠檢測傳統(tǒng)模型檢測工具無法檢測的知識邏輯屬性,同時與其它模型檢測工具進(jìn)行了比較,證明了本文工具的正確性和高效性。
　　(2)首次用時態(tài)認(rèn)知邏輯模型檢測技術(shù)對Web服務(wù)的特征交互問題進(jìn)行了形式化驗證。用MCTK對在線股票交易系統(tǒng)服務(wù)STS協(xié)議的特征交互問題進(jìn)行了分析和驗證,發(fā)現(xiàn)了STS協(xié)議中的特征沖突現(xiàn)象,驗證了STS協(xié)

5、議的特征沖突屬性。
　　(3)提出了從Web服務(wù)的描述語言BPEL到本文的模型檢測工具(MCTK)的形式化驗證框架。給出了從Web服務(wù)的過程描述模型(BPEL)到形式化模型(有限狀態(tài)機模型)的轉(zhuǎn)換框架,這將使得Web服務(wù)的形式化驗證工作更加自動化。
　　(4)用時態(tài)認(rèn)知邏輯模型檢測技術(shù)對安全協(xié)議進(jìn)行了形式化驗證。用MCTK對經(jīng)典的Needham-Schroeder協(xié)議進(jìn)行了分析和驗證,找到了該協(xié)議的漏洞,并且與其它工具進(jìn)行了