基于XYZ-ADL的Web服務(wù)組合驗(yàn)證研究.pdf

1、隨著互聯(lián)網(wǎng)和電子商務(wù)技術(shù)的發(fā)展,Web服務(wù)因其能解決Internet異構(gòu)平臺下服務(wù)的交互重用等問題引起了廣泛關(guān)注。和傳統(tǒng)的分布式計(jì)算模型相比,Web服務(wù)抽象程度更高、粒度更大、獨(dú)立性更強(qiáng),但是單一的Web服務(wù)功能有限,難以滿足不斷變化的業(yè)務(wù)需求,因此有必要對多個(gè)Web服務(wù)進(jìn)行組合以提供更強(qiáng)大的功能。由于Web服務(wù)組合常用于描述跨平臺跨組織的高層業(yè)務(wù)邏輯,因此保證其正確性就顯得更為重要。
　　 Web服務(wù)組合是Web服務(wù)領(lǐng)域的研究

2、熱點(diǎn),目前雖然有多種正確性驗(yàn)證方法,但從體系結(jié)構(gòu)方面驗(yàn)證Web服務(wù)組合,則是一個(gè)新的研究方向。精化檢驗(yàn)和模型檢測是兩種重要的形式驗(yàn)證技術(shù),本文把兩者應(yīng)用到Web服務(wù)領(lǐng)域驗(yàn)證Web服務(wù)組合的正確性。
　　 基于上述思想,本文在課題組已有工作基礎(chǔ)上,研究基于形式化方法和軟件體系結(jié)構(gòu)描述語言XYZ/ADL的Web服務(wù)組合驗(yàn)證問題。XYZ/ADL是時(shí)序邏輯語言XYZ/E的擴(kuò)展,對有時(shí)間約束的系統(tǒng)而言,可由XYZ/E的實(shí)時(shí)擴(kuò)展語言即XYZ

3、/RE表示系統(tǒng)應(yīng)滿足的時(shí)間約束。考慮到多數(shù)Web服務(wù)具有實(shí)時(shí)特征,本文分析XYZ/RE和時(shí)間自動(dòng)機(jī)組成元素的相似性,改進(jìn)XYZ/RE到時(shí)間自動(dòng)機(jī)的映射規(guī)則。針對Web服務(wù)組合系統(tǒng),分別用XYZ/ADL描述其行為和性質(zhì),再將其中的XYZ/RE分別轉(zhuǎn)換為對應(yīng)的行為時(shí)間自動(dòng)機(jī)和性質(zhì)時(shí)間自動(dòng)機(jī),通過精化檢驗(yàn)的方法判斷Web服務(wù)組合系統(tǒng)的行為是否符合性質(zhì)需求。另一方面,將單個(gè)Web服務(wù)XYZ/ADL描述中的XYZ/RE映射至單個(gè)時(shí)間自動(dòng)機(jī),多個(gè)W