基于語(yǔ)言的軟件可信性度量理論及其應(yīng)用.pdf

1、軟件是信息基礎(chǔ)設(shè)施的靈魂.隨著軟件規(guī)模的日趨龐大，軟件的可信性越來越引起人們的關(guān)注?？尚跑浖A(chǔ)研究已經(jīng)成為國(guó)內(nèi)外研究的一個(gè)熱點(diǎn)，軟件可信性度量的研究是其中一個(gè)重要研究?jī)?nèi)容。軟件可信性度量的研究，需要有合適的度量方法，以形式化理論為基礎(chǔ)建立軟件的可信性度量理論與模型，從而給出對(duì)軟件可信性的評(píng)價(jià)，使其能成為反映軟件品質(zhì)及其產(chǎn)品競(jìng)爭(zhēng)力的一個(gè)重要指標(biāo).另一方面，在開放的網(wǎng)絡(luò)環(huán)境下，軟件系統(tǒng)的可信性受到了更大的挑戰(zhàn)，軟件系統(tǒng)的降級(jí)替換是研究提高

2、其可信性的方法之一，而保證降級(jí)替換的正確性、評(píng)價(jià)降級(jí)替換的可信程度等問題也將是軟件可信性度量研究的重要內(nèi)容。
　　 本文基于語(yǔ)言對(duì)軟件系統(tǒng)的可信性進(jìn)行形式化刻畫和度量，主要的貢獻(xiàn)可以概括為以下幾方面：
　　 ■理論：(1)隨機(jī)-混成進(jìn)程代數(shù)(stochastic-Hybrid CSP，S-HCSP)可信性量化理論。將隨機(jī)因素引入HCSP，得到修改后的語(yǔ)言稱為S-HCSP。基于S-HCSP，先對(duì)其原子構(gòu)造形式化地定義可信度

3、，再利用經(jīng)濟(jì)學(xué)的木桶原理和太極圖的陰陽(yáng)轉(zhuǎn)化平衡原理等對(duì)其算子定義可信度計(jì)算規(guī)則，從而建立S-HCSP的可信性量化理論；(2)概率擬Hoare邏輯(Probabilistic Quasi-Hoare Logic，PQHL)可信性量化理論。在Hoare邏輯(Hoare Logic，HL)的基礎(chǔ)上提出PQHL，用于刻畫程序的可信度，定量地描述理論與程序?qū)嶋H執(zhí)行之間的差距，反映理論被程序?qū)崿F(xiàn)的程度，從而量化理論上正確的程序在實(shí)際執(zhí)行時(shí)出錯(cuò)的可能

4、性以及解釋可信度很高兩個(gè)程序(或是構(gòu)件)的串行復(fù)合之后可信度可能并不高等問題.證明了一種特殊概率擬Hoare邏輯-[α1，α2]1-擬Hoare邏輯的可靠性，并進(jìn)一步分析了PQHL的思想背景及其與Hoare邏輯之間的關(guān)系；(3)Web服務(wù)降級(jí)替換可信性量化理論。在原有進(jìn)程代數(shù)基礎(chǔ)上添加超時(shí)處理算子和延時(shí)處理算子，從而給出了Web服務(wù)降級(jí)替換的一致性條件，保證了Web服務(wù)降級(jí)替換的合成正確性，進(jìn)一步研究了Web服務(wù)降級(jí)替換的可信程度，建立

5、了Web服務(wù)降級(jí)替換的可信性量化理論。
　　 ■應(yīng)用：(1)將建立S-HCSP可信性量化理論的組合分析方法應(yīng)用到基于語(yǔ)言的軟件以及Web服務(wù)可信性度量的研究，分別建立了基于結(jié)構(gòu)化程序設(shè)計(jì)語(yǔ)言的軟件可信性度量模型和基于BPEL(Business Process Execution Language)的Web服務(wù)可信性度量模型；(2)將PQHL應(yīng)用到基于構(gòu)件的軟件可信性度量的研究。以PQHL為理論基礎(chǔ)，提出一種通過比較需求前置、后置

6、與構(gòu)件前置、后置之間差別來評(píng)價(jià)構(gòu)件對(duì)需求實(shí)現(xiàn)程度的近似匹配度量方法。然后，通過復(fù)用構(gòu)件之間的約束關(guān)系(順序組裝、選擇組裝和重復(fù)組裝)，建立基于構(gòu)件的軟件可信性度量模型。
　　 ■工具：以基于結(jié)構(gòu)化程序設(shè)計(jì)語(yǔ)言的軟件可信性度量模型為基礎(chǔ)，利用Ruby/Tk開發(fā)了一個(gè)軟件可信性度量的工具一軟件可信性度量可視化工具(Software Trustworthiness Measurement Visual Tool，STMVT).通過ST