軟件行為運行時驗證研究.pdf

1、隨著軟件系統(tǒng)在電信、金融等領(lǐng)域的廣泛應(yīng)用，軟件系統(tǒng)規(guī)模越來越龐大，軟件結(jié)構(gòu)與軟件行為日益復(fù)雜，人們對其正確性、可用性、可靠性和安全性等可信性質(zhì)提出了更高的要求和期望。論文分析了傳統(tǒng)的軟件質(zhì)量保證方式，如：測試、驗證以及運行時驗證的特點。提出一種以軟件運行行為為關(guān)注點的運行時驗證與分析思想。
　　討論了軟件行為描述技術(shù)，設(shè)計了一種行為模式描述語言(BPDL)，并給出了BPDL到確定狀態(tài)自動機的自動轉(zhuǎn)換方法。BPDL是一種簡潔的、描述

2、能力很強的語言，它可以對軟件運行行為蹤跡進行形式化描述，同時BPDL還可以用于描述軟件行為規(guī)約。同以往描述語言不同，BPDL把軟件之間復(fù)雜的交互行為看作是事件序列及行為約束，從而簡化了交互行為描述的復(fù)雜性，便于對軟件行為進行運行時驗證和分析。
　　研究了軟件運行時驗證技術(shù)，提出了一個軟件行為運行時驗證框架。在該框架中對軟件行為的驗證分兩個階段進行。首先采用自動機原理驗證單一事件序列是否符合行為規(guī)約，當違反行為規(guī)約的事件出現(xiàn)時，驗證

3、系統(tǒng)給出相應(yīng)提示；然后，對與歷史信息相關(guān)的復(fù)雜交互行為的驗證則采用多實體貝葉斯網(wǎng)技術(shù)進行驗證分析，通過交互實體運行期的實時經(jīng)歷和以往經(jīng)歷進行知識融合對交互實體的可信性進行實時地自動計算，對當前交互行為是否可信做出實時和客觀地判斷。該框架對交互行為的監(jiān)測可靈活配置，驗證分兩個階段進行既能有效減少對軟件系統(tǒng)的性能影響，提高驗證效率，又能保證驗證分析的準確性。
　　實現(xiàn)了軟件運行時行為驗證原型系統(tǒng)，并在典型的應(yīng)用環(huán)境中加以測試。詳細闡述