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

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

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

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

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

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