1、鄭州大學(xué)博士學(xué)位論文形式化方法在構(gòu)件組裝實時系統(tǒng)中的應(yīng)用研究姓名：席琳申請學(xué)位級別：博士專業(yè)：計算機軟件與理論指導(dǎo)教師：周清雷201204摘要統(tǒng)的組裝實例展示了這個方法及其效果。該方法的顯著特點是建模精確，另外UPPAAL用動態(tài)驗證技術(shù)和符號技術(shù)減少驗證問題的規(guī)模，從而使該方法可以用于相當(dāng)規(guī)模的系統(tǒng)組裝。(3)提出了三個針對實時系統(tǒng)的測試用例覆蓋標(biāo)準(zhǔn)，自動生成長度優(yōu)化的測試用例并給出了實例分析。根據(jù)實時系統(tǒng)的特點，在滿足組裝行為相容性的

2、前提下，針對實時系統(tǒng)的安全屬性和時間屬性這兩個重要的可信屬性定義了兩個新的測試覆蓋標(biāo)準(zhǔn)，針對重要組裝行為定義了相容性覆蓋標(biāo)準(zhǔn)，然后將這三個覆蓋標(biāo)準(zhǔn)轉(zhuǎn)化為模型檢測工具UPPAAL中對性質(zhì)進行描述的斷言形式，最后利用UPPAAL工具的生成最短診斷路徑的功能自動生成長度優(yōu)化的測試用例。面向性質(zhì)測試比非面向性質(zhì)測試進行得更深入，因此，該方法產(chǎn)生的測試用例比傳統(tǒng)的、測試用例更高效、覆蓋率更高。(4)提出了一種利用軟件體系結(jié)構(gòu)信息和可信等級化度量來

3、選擇構(gòu)件并估計系統(tǒng)可靠性的方法。首先，根據(jù)構(gòu)件軟件及基于構(gòu)件軟件開發(fā)的層次性特征，用層次自動機對構(gòu)件及整個軟件系統(tǒng)進行形式化描述，用構(gòu)件關(guān)系矩陣描述構(gòu)件模塊之間交互的頻度，計算構(gòu)件模塊重要度因子，然后，根據(jù)重要程度不同，用重要度因子分級函數(shù)和等級質(zhì)量映射函數(shù)來指導(dǎo)選擇不同可信特性的構(gòu)件組裝系統(tǒng)并以此為基礎(chǔ)對構(gòu)件組裝軟件進行可靠性分析。最后，結(jié)合一個實例展示了這種方法的具體使用。構(gòu)件組裝相容性驗證方法從行為層面指導(dǎo)構(gòu)件選擇，該方法更進一步