軟件可信驗(yàn)證自動(dòng)化技術(shù)研究.pdf

1、缺陷和漏洞廣泛存在于各種軟件中，難以避免，由其引發(fā)的故障很容易給生命財(cái)產(chǎn)帶來(lái)?yè)p害，甚至災(zāi)難性后果。應(yīng)對(duì)這一問(wèn)題的有效途徑是設(shè)計(jì)有效合理的自動(dòng)化的測(cè)試方法對(duì)軟件系統(tǒng)可信度進(jìn)行充分全面的驗(yàn)證。本論文對(duì)軟件可信安全性驗(yàn)證研究從靜態(tài)驗(yàn)證和動(dòng)態(tài)檢測(cè)兩個(gè)角度分別著手。
　　首先從靜態(tài)檢測(cè)角度，針對(duì)安全苛刻性編程標(biāo)準(zhǔn)，提出基于規(guī)則匹配的代碼靜態(tài)檢測(cè)方法。構(gòu)建易于表述及存儲(chǔ)源碼信息的源碼表示模型，解決C++語(yǔ)言的靈活性和復(fù)雜性導(dǎo)致的難以對(duì)代碼直接

2、進(jìn)行規(guī)則匹配的問(wèn)題;設(shè)計(jì)解析樹(shù)模型和存儲(chǔ)轉(zhuǎn)換模型，完成從源代碼提取與規(guī)則有關(guān)的信息翻譯為中間表示文件的源碼解析過(guò)程;設(shè)計(jì)包含編程安全標(biāo)準(zhǔn)中全部有效規(guī)則的規(guī)則庫(kù)模型用于對(duì)中間表示文件進(jìn)行規(guī)則匹配和缺陷反饋;通過(guò)系統(tǒng)實(shí)現(xiàn)和實(shí)驗(yàn)驗(yàn)證方法的有效性。
　　然后從動(dòng)態(tài)檢測(cè)角度，提出一種基于非確定性FSM模型的測(cè)試生成和測(cè)試驗(yàn)證方法。針對(duì)復(fù)雜軟件系統(tǒng)狀態(tài)行為轉(zhuǎn)換不確定的問(wèn)題，提出層次化建模方法，對(duì)不確定的狀態(tài)轉(zhuǎn)移進(jìn)行聚類和分層建模，將其轉(zhuǎn)化為分

3、層子狀態(tài)機(jī)間確定唯一的狀態(tài)轉(zhuǎn)移，解決軟件設(shè)計(jì)規(guī)格不確定行為難以描述和生成測(cè)試用例的問(wèn)題;提出從正則式模型產(chǎn)生測(cè)試集的方法，根據(jù)狀態(tài)機(jī)與正則表達(dá)式的等價(jià)關(guān)系，構(gòu)建狀態(tài)機(jī)模型對(duì)應(yīng)的的正則式模型，給出遷移覆蓋算法從正則式模型生成測(cè)試集，解決軟件系統(tǒng)控制流程中循環(huán)部分在用例中難以精確描述的問(wèn)題;在正則式模型中加入不同觸發(fā)參數(shù)作為用例特征，劃分出不同特征的測(cè)試集，提高用例的驗(yàn)證能力和測(cè)試充分性。
　　靜態(tài)手段可以在軟件開(kāi)發(fā)早期發(fā)現(xiàn)程序中的潛