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

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

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

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