網(wǎng)構軟件系統(tǒng)構建的形式化分析研究.pdf

1、隨著Internet廣泛應用和普及,軟件開發(fā)、部署、運行和維護的計算平臺已經(jīng)逐步由封閉、靜態(tài)、可控走向開放、動態(tài)、難控。Internet平臺上軟件系統(tǒng)已經(jīng)呈現(xiàn)為柔性可演化、連續(xù)反應式、多目標適應的新形態(tài)。中國軟件工程領域?qū)⑦@樣一種新的軟件形態(tài)稱之為網(wǎng)構軟件。本文對網(wǎng)構軟件的構造過程以及網(wǎng)構軟件整個生命周期進行研究,基于抽象狀態(tài)機理論提出一套適合分析、構造以及驗證可靠網(wǎng)構軟件系統(tǒng)的形式化模型,同時給出普適環(huán)境下智能家庭系統(tǒng)的原型案例。

2、r>　　 論文的主要研究工作和創(chuàng)新性包含以下幾個方面:
　　 (1)本文采用分布式抽象狀態(tài)機進行刻畫目標網(wǎng)構軟件系統(tǒng),建立分布式抽象狀態(tài)機與網(wǎng)構軟件之間的映射關系,在這個模型中每個子抽象狀態(tài)機對應為網(wǎng)絡平臺中的一個構件,而構件內(nèi)部的輸入輸出又進一步分解成子抽象狀態(tài)機,它們之間通過監(jiān)督函數(shù)進行交互。在該環(huán)境中,除了構件本身,其它所有與此構件有交互關系的構件及網(wǎng)絡狀況都構成了該構件的運行環(huán)境。環(huán)境中的普通函數(shù)通過成為該構件子狀態(tài)機

3、中的監(jiān)督函數(shù)來對該構件提供環(huán)境信息。通過這些映射關系,建立了基于抽象狀態(tài)機的網(wǎng)構軟件模型。該模型具有可抽象執(zhí)行驗證的特征,使得目標系統(tǒng)在需求高抽象層次各種屬性能夠得到驗證。在模型中對構件之間的交互模式,交互仲裁模型等進行了詳細的分析,該模型的建立使得網(wǎng)構軟件在構造之前需求能夠準確清晰。
　　 (2)由于采用抽象狀態(tài)機刻畫網(wǎng)構軟件系統(tǒng)往往從抽象程度極高的自然層次開始,為了使模型能夠逐步向可執(zhí)行的目標系統(tǒng)逼近,本文提出基于抽象狀態(tài)機

4、網(wǎng)構軟件抽象模型的精化機制,并給出交互模式的精化模型和構件精化模型。通過研究基于抽象狀態(tài)機網(wǎng)構軟件抽象模型的通用精化機制,本文進一步給出了智能家庭體系結構中協(xié)作模型的精化模型以及基于OSGi的普適網(wǎng)構基礎平臺的精化模型。在這些模型中保證了精化步驟不丟失或變化系統(tǒng)的原有特性和性質(zhì),從而確保精化的正確性,最終保證高層次抽象網(wǎng)構軟件模型與最終網(wǎng)構軟件模型的一致性。
　　 (3)為了在網(wǎng)構軟件設計的早期階段盡量的避免和消除錯誤,本文采用

5、抽象狀態(tài)機的可抽象執(zhí)行機制,提出網(wǎng)構軟件精化設計過程中在不同抽象層次的可執(zhí)行驗證模型。因此,通過該模型可以在不同的抽象層次對網(wǎng)構軟件設計模型進行模擬執(zhí)行,從而盡早的發(fā)現(xiàn)設計中的問題,在設計的早期階段保證軟件的正確性,避免后期錯誤帶來的巨大損失。另一方面,為了在設計的精化過程中不丟失目標系統(tǒng)的各種屬性,精化前后保持一致性,本文提出了基于抽象狀態(tài)機的網(wǎng)構軟件模型精化驗證模型,通過該模型能夠確保設計精化過程的正確性,由此也可以由過程的正確性來

6、保證目標系統(tǒng)的正確性。
　　 (4)為了采用網(wǎng)構軟件理論有效的解決普適計算領域中的問題以及使網(wǎng)構軟件理論在新的領域進一步得到驗證和豐富,本文采用OSGi和R-OSGi作為普適網(wǎng)構軟件平臺,并提出合理的智能家庭體系結構。在該結構中,結合R-OSGi技術優(yōu)點給出了三種重要的協(xié)作模型:a)直接服務請求協(xié)作模型,b)基于遠程事件的發(fā)布/訂閱形成的協(xié)作模型,c)被動協(xié)作模型,并且在原型系統(tǒng)中得到了實現(xiàn)。通過系統(tǒng)實驗驗證可以看出,本體系結構