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

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

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

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