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

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

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

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

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

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