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

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

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

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

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

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

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