實時服務(wù)構(gòu)件的語義特征和行為組裝形式化技術(shù)研究.pdf

1、在面向服務(wù)的架構(gòu)中，如何根據(jù)系統(tǒng)資源環(huán)境的變化以及構(gòu)件的功能和實時性等QoS屬性動態(tài)組合已有的功能構(gòu)件以滿足應(yīng)用需求，成為當(dāng)前此領(lǐng)域的一個研究熱點。由于采用非形式化(自然語言)和半形式化(圖表)方法描述實時服務(wù)系統(tǒng)均存在不精確、歧義的及不易驗證等缺陷，而形式化方法能較好地克服上述不足，可充分表述系統(tǒng)的各種特性，并為系統(tǒng)的驗證、實現(xiàn)等提供良好的基礎(chǔ)。 本文提出了一種結(jié)合OCL與HTA的實時服務(wù)構(gòu)件(Real-Time Servic

2、e Component)形式化描述方法：用OCL描述構(gòu)件的靜態(tài)語義特征，用HTA描述構(gòu)件的動態(tài)抽象行為；前者為后者的正確性提供屬性約束，后者提供前者所描述需求的具體實現(xiàn)，兩者語義互補(bǔ)。主要內(nèi)容及其貢獻(xiàn)包括： (1)提出一種基于特征的構(gòu)件語義描述模型，首先分別給出特征、特征空間和構(gòu)件特征空間表示模型的定義。接著將構(gòu)件特征間的各種關(guān)聯(lián)和依賴關(guān)系分成自身約束、父子關(guān)系約束、顯性約束和隱性約束四類，并采用對象約束語言對這些關(guān)系進(jìn)行形式化

3、描述，從而為模型提供了精確的語義支持。面向電子商務(wù)的構(gòu)件特征子樹的實例研究及其模型驗證和實驗結(jié)果證明了該模型的正確性與有效性。 (2)采用HTA形式化描述實時服務(wù)構(gòu)件的動態(tài)抽象行為。給出實時服務(wù)構(gòu)件的HTA模型，系統(tǒng)闡述構(gòu)件間的各種組裝方式及其形式模型，分析構(gòu)件組裝的語法可組合性和語義可組合性問題。采用HTA可層次地構(gòu)造實時系統(tǒng)集成框架，較高層次的實時服務(wù)構(gòu)件的行為可通過由較低層次的構(gòu)件組成的HTA來定義。該模型的顯著特點是簡單

4、容易理解，能在一個統(tǒng)一的框架中表示構(gòu)件的組裝、行為和分析系統(tǒng)性能，適用于不同粒度的實時服務(wù)構(gòu)件集成，有效降低了實時服務(wù)系統(tǒng)的復(fù)雜度，從而使模型驗證工具能夠處理更為復(fù)雜的服務(wù)系統(tǒng)。 (3)提出一種基于MLTS的實時服務(wù)構(gòu)件HTA模型組裝驗證算法。給出(層次)自動機(jī)到標(biāo)號遷移系統(tǒng)的轉(zhuǎn)換過程，在標(biāo)號遷移系統(tǒng)的擴(kuò)展模型一多集標(biāo)號遷移系統(tǒng)基礎(chǔ)上，給出其組裝算法，利用共享動作是否轉(zhuǎn)換為內(nèi)部動作來判定模型的組裝兼容性。該算法能夠有效降低狀態(tài)空

5、間爆炸給模型實例檢測帶來的難度，同時利用了MLTS能夠描述系統(tǒng)同步、異步動作的特點，不僅可以跟蹤構(gòu)件組裝前后的狀態(tài)變化，而且能夠刻畫構(gòu)件的接口行為動作變化，因此，它在基于HTA的實時服務(wù)構(gòu)件模型組裝兼容性驗證方面具有較強(qiáng)的表達(dá)能力。 (4)描述一個較簡單但又具有典型實時服務(wù)系統(tǒng)特征的小額支付視頻點播實例應(yīng)用系統(tǒng)。首先采用自頂向下的方法構(gòu)建系統(tǒng)，接著采用本文的描述方法對系統(tǒng)級的構(gòu)件及其組裝進(jìn)行建模、分析和驗證，并簡單分析了系統(tǒng)的時