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

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

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

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

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

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

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