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

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

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

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

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

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