普適環(huán)境下基于抽象狀態(tài)機(jī)的服務(wù)組合的分析與驗(yàn)證.pdf

1、自20世紀(jì)90年代Weiser[1,2]提出“普適計(jì)算”概念以來(lái),嵌入式系統(tǒng),無(wú)線通信等技術(shù)的發(fā)展為“服務(wù)無(wú)時(shí)不在,無(wú)處不在”的普適計(jì)算從理論變成現(xiàn)實(shí)提供了客觀的技術(shù)基礎(chǔ)。普適計(jì)算的目標(biāo)是將由網(wǎng)絡(luò)和傳感器以及移動(dòng)設(shè)備組成的信息空間和現(xiàn)在的物理空間結(jié)合起來(lái),支持用戶隨時(shí)隨地獲取所需的服務(wù)。因此如何在普適環(huán)境下進(jìn)行有效的服務(wù)組合逐漸成為了一個(gè)熱點(diǎn)。
　　在普適環(huán)境下,不僅有網(wǎng)絡(luò)上的web服務(wù),還有傳感器和移動(dòng)設(shè)備等提供的設(shè)備服務(wù)以及各

2、類其他的服務(wù),結(jié)合SOA思想[3],共同組成了組合服務(wù)并將其最終構(gòu)建應(yīng)用模型。但是,由于普適計(jì)算環(huán)境所具有的自治性,動(dòng)態(tài)性和設(shè)備資源的約束性,使得在這樣的環(huán)境下進(jìn)行服務(wù)組合時(shí)面臨著特有的問(wèn)題和挑戰(zhàn)[4],比如服務(wù)組合過(guò)程中錯(cuò)誤的處理、檢測(cè),比如設(shè)備的動(dòng)態(tài)加入和刪除等。因此在普適環(huán)境中,如何為用戶提供可信的服務(wù)組合成為了普適環(huán)境下服務(wù)組合的關(guān)鍵問(wèn)題。
　　本文分析了已有的服務(wù)組合的技術(shù)以及服務(wù)組合模型,并在此基礎(chǔ)上提出了一個(gè)基于抽象

3、狀態(tài)機(jī)的服務(wù)組合模型,并提出驗(yàn)證方法。使用抽象狀態(tài)機(jī)對(duì)服務(wù)的行為進(jìn)行刻畫,能夠很好地對(duì)服務(wù)進(jìn)行不同精化層級(jí)上的形式化描述,從而達(dá)到不同層級(jí)的正確性驗(yàn)證需求。然后結(jié)合 SPIN進(jìn)行安全性、可達(dá)性的模型檢測(cè)。最后本文在實(shí)驗(yàn)中利用工具CoreASM和SPIN對(duì)文中提出的服務(wù)組合模型進(jìn)行驗(yàn)證,從而保證服務(wù)組合的正確性。實(shí)驗(yàn)結(jié)果表明,我們所提出的服務(wù)組合模型和驗(yàn)證方法能夠較好地適應(yīng)普適環(huán)境下服務(wù)組合系統(tǒng)的需求,驗(yàn)證其正確性,對(duì)后續(xù)的基于這樣的服務(wù)