可信普適服務(wù)的形式化分析與驗證.pdf

1、普適計算通常是在一個動態(tài)、異構(gòu)、開放的物理環(huán)境下進行，其中不少物理設(shè)備的資源受限、高移動性以及故障頻發(fā)，這些特征給構(gòu)建可信的普適服務(wù)帶來了新的挑戰(zhàn)。本文針對普適環(huán)境下如何構(gòu)建可信的普適服務(wù)進行研究，從普適服務(wù)模型的特征分析著手,提出了一種描述該模型的形式化語言，設(shè)計了面向普適應(yīng)用的類型和效果系統(tǒng)，用于抽取所構(gòu)建的普適服務(wù)的動態(tài)行為，進而形式化分析行為一致的服務(wù)替換;對于普適服務(wù)之間復(fù)雜的交互行為進行形式化建模，利用模型檢驗技術(shù)對普適服務(wù)

2、的行為屬性進行驗證；另外還提出了一種普適環(huán)境下的動態(tài)服務(wù)更新框架，以滿足復(fù)雜動態(tài)環(huán)境的需求，并抽象出該框架的形式化模型及驗證其屬性；最后構(gòu)建了典型的普適應(yīng)用場景對本文所提出的方法進行驗證，實驗結(jié)果表明該方法的可行性和有效性。
　　本文的主要工作和創(chuàng)新性包括以下幾個方面：
　　（1）本文在研究服務(wù)構(gòu)件模型的基礎(chǔ)上，著重分析了服務(wù)的接口類型和行為語義，并考慮了復(fù)雜普適環(huán)境下服務(wù)實體（設(shè)備）的遷移性和可變性，提出了一種普適環(huán)境下的

3、服務(wù)模型，它具有上下文感知接口、資源訪問協(xié)議以及可組合性的特征，能夠適應(yīng)普適環(huán)境的動態(tài)性和滿足可信性需求。
　?。?）擴展類型化λ演算以描述服務(wù)模型，針對復(fù)雜普適環(huán)境下服務(wù)的組合模式，提出一種面向普適應(yīng)用的類型和效果系統(tǒng)，運用該系統(tǒng)中的子類型技術(shù)來分析行為一致的服務(wù)替換，并推導出類型安全性定理。該定理確保了所替換服務(wù)的行為是合法的，并且利用Coq輔助證明工具驗證了本定理的證明過程是正確的、可信的。
　?。?）利用類型和效果系

4、統(tǒng)技術(shù)以抽取出服務(wù)的動態(tài)行為，將它們轉(zhuǎn)換為相應(yīng)的服務(wù)流程有限狀態(tài)機；進而可將服務(wù)抽象為一種進程模型，利用模型檢驗工具來自動驗證所組合服務(wù)的行為屬性（例如，安全性、活性），以確認它們符合給定的行為策略，從而確保該服務(wù)組合是可信的、有效的。
　　（4）為了適應(yīng)普適環(huán)境的動態(tài)性和滿足不斷變化的用戶需求，提出了一種普適環(huán)境下的動態(tài)服務(wù)更新框架，以支持所構(gòu)建普適應(yīng)用的在線維護及動態(tài)演化。本文定義了該框架的形式化模型，利用模型檢驗工具來驗證其

5、屬性（例如，透明性、正確性等），并且證明了動態(tài)服務(wù)更新也符合類型安全更新的要求；在此基礎(chǔ)上，設(shè)計出了相應(yīng)的動態(tài)更新系統(tǒng)以支持普適應(yīng)用的在線更新；該系統(tǒng)不但能夠處理動態(tài)接口適應(yīng)性，而且支持更新失敗的恢復(fù)。實驗表明：在更新過程中，該框架給普適應(yīng)用所造成的性能損失是有限的，并且能夠滿足動態(tài)服務(wù)更新的需求。
　　（5）基于OSGi服務(wù)平臺及支持分布式的R-OSGi中間件技術(shù)構(gòu)建出典型的普適應(yīng)用場景，以驗證本文的理論方法和技術(shù)方案的可行性和