基于最弱前置條件的程序正確性分析
摘要：隨著軟件的不斷更新迭代,軟件正確性檢測(cè)的必要性愈加凸顯,軟件正確性檢測(cè)的處理時(shí)間直接決定軟件的維護(hù)成本。動(dòng)態(tài)測(cè)試的斷言編寫和靜態(tài)分析的符號(hào)執(zhí)行均針對(duì)程序正確性進(jìn)行優(yōu)化完善,但分析結(jié)果易出現(xiàn)路徑缺失甚至錯(cuò)誤無(wú)法識(shí)別等問題。現(xiàn)有驗(yàn)證方法在路徑擴(kuò)展時(shí)易生成較多無(wú)用路徑,且針對(duì)性不強(qiáng),因此有必要研究一種更為可靠的方案。本文采用最弱前置條件對(duì)軟件可行性加以分析,對(duì)程序執(zhí)行語(yǔ)義正確建模,使用程序切片技術(shù)預(yù)處理程序代碼,并根據(jù)層級(jí)結(jié)構(gòu)存儲(chǔ)節(jié)點(diǎn)及其子程序。實(shí)驗(yàn)結(jié)果表明,該方法可以有效減小靜態(tài)分析對(duì)程序狀態(tài)抽象操作帶來(lái)的驗(yàn)證精度損耗,且能夠遍歷求解出程序的所有可能路徑,并通過分組標(biāo)出條件表達(dá)式的結(jié)論真假值,以此驗(yàn)證路徑正確性,同時(shí)可對(duì)高復(fù)雜的程序代碼進(jìn)行有效的正確性分析。
注：因版權(quán)方要求，不能公開全文，如需全文，請(qǐng)咨詢雜志社。
高技術(shù)通訊雜志
高技術(shù)通訊雜志， 月刊，本刊重視學(xué)術(shù)導(dǎo)向，堅(jiān)持科學(xué)性、學(xué)術(shù)性、先進(jìn)性、創(chuàng)新性，刊載內(nèi)容涉及的欄目：計(jì)算機(jī)與通信技術(shù)、先進(jìn)制造與自動(dòng)化、專利分析技術(shù)等。于1991年經(jīng)新聞總署批準(zhǔn)的正規(guī)刊物。
- 統(tǒng)計(jì)源期刊
- 1-3個(gè)月審核
