形式化方法在構件組裝實時系統(tǒng)中的應用研究.pdf

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

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

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