形式化方法在構(gòu)件組裝實(shí)時(shí)系統(tǒng)中的應(yīng)用研究.pdf

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

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

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