發(fā)布時(shí)間：2018-11-07 18:27

【摘要】：采用形式化方法證明軟件的正確性,是保障軟件可靠性的有效方法.而對循環(huán)語句的分析與驗(yàn)證,是形式化證明中的關(guān)鍵,對循環(huán)語句的處理一直是程序分析與驗(yàn)證中的一個(gè)難點(diǎn)問題.提出使用循環(huán)語句修改的內(nèi)存和這些內(nèi)存中存放的新值來描述循環(huán)語句的執(zhí)行效果,并將該執(zhí)行效果定義為循環(huán)摘要.同時(shí),提出一種自動(dòng)生成循環(huán)摘要的方法,可以為操作常用數(shù)據(jù)結(jié)構(gòu)的循環(huán)自動(dòng)生成循環(huán)摘要,包含嵌套循環(huán).此外,基于循環(huán)摘要,可以自動(dòng)生成循環(huán)語句的規(guī)約,包括循環(huán)不變式、循環(huán)的前置條件以及循環(huán)的后置條件.已經(jīng)實(shí)現(xiàn)了自動(dòng)生成循環(huán)摘要以及循環(huán)規(guī)約的方法,并將它們集成到驗(yàn)證工具Accumulator中.實(shí)驗(yàn)結(jié)果表明,該方法可以有效地生成循環(huán)摘要,并生成多種類型的規(guī)約,從而輔助軟件程序的形式化證明,提高驗(yàn)證的自動(dòng)化程度和效率,減輕驗(yàn)證人員的負(fù)擔(dān).
[Abstract]:Using formal method to prove the correctness of software is an effective method to guarantee the reliability of software. The analysis and verification of circular statements is the key to formal proof, and the processing of circular statements is always a difficult problem in program analysis and verification. The memory modified by the loop statement and the new values stored in the memory are proposed to describe the execution effect of the loop statement, and the execution effect is defined as a loop summary. At the same time, a method of generating loop summary automatically is proposed, which can generate loop summary automatically for the loop of common data structure, including nested loop. In addition, based on the loop summary, the specification of the loop statement can be generated automatically, including the loop invariant, the precondition of the loop and the post-condition of the loop. The method of automatically generating loop summary and loop specification has been implemented and integrated into the verification tool Accumulator. The experimental results show that this method can effectively generate circular abstracts and generate various kinds of protocols, which can help the formal proof of software programs, improve the automation and efficiency of verification, and reduce the burden on verifiers.
【作者單位】： 計(jì)算機(jī)軟件新技術(shù)國家重點(diǎn)實(shí)驗(yàn)室(南京大學(xué));南京大學(xué)軟件學(xué)院;南京大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)系;
【基金】：國家自然科學(xué)基金(61632015,61561146394) 國家重點(diǎn)研發(fā)計(jì)劃(2016YFB1000802)~~
【分類號】：TP311

【參考文獻(xiàn)】

相關(guān)期刊論文 前6條

1 聶楚江;劉海峰;蘇璞睿;馮登國;;一種面向程序動(dòng)態(tài)分析的循環(huán)摘要生成方法[J];電子學(xué)報(bào);2014年06期

2 劉自恒;曾慶凱;;一種自適應(yīng)的循環(huán)不變式生成方法[J];計(jì)算機(jī)工程;2013年06期

3 劉剛;陳意云;張志天;;循環(huán)不變形狀圖的自動(dòng)推斷[J];電子技術(shù);2011年08期

4 邢建英;李夢君;李舟軍;;CILinear:一個(gè)線性不變式自動(dòng)構(gòu)造工具[J];計(jì)算機(jī)科學(xué);2010年12期

5 馬竹根;王燦明;;利用基因表達(dá)式編程自動(dòng)生成循環(huán)不變式[J];計(jì)算機(jī)與數(shù)字工程;2009年07期

6 畢忠勤;曾振柄;郭遠(yuǎn)華;;非線性循環(huán)不變式的自動(dòng)生成[J];計(jì)算機(jī)應(yīng)用;2008年07期

【相似文獻(xiàn)】

相關(guān)期刊論文 前10條

1 楊淑群,吳文兵,丁樹良;從集合論的角度分析循環(huán)不變式[J];吉林化工學(xué)院學(xué)報(bào);2005年03期

2 畢忠勤;曾振柄;郭遠(yuǎn)華;;非線性循環(huán)不變式的自動(dòng)生成[J];計(jì)算機(jī)應(yīng)用;2008年07期

3 劉自恒;曾慶凱;;一種自適應(yīng)的循環(huán)不變式生成方法[J];計(jì)算機(jī)工程;2013年06期

4 游曉明,劉升;試論循環(huán)不變式和囿界函數(shù)在循環(huán)研制中的地位和作用[J];湖北師范學(xué)院學(xué)報(bào)(自然科學(xué)版);1998年06期

5 王曉東,吳英杰,傅仰耿,傅志祥;算法歸納設(shè)計(jì)策略與循環(huán)不變式[J];福州大學(xué)學(xué)報(bào)(自然科學(xué)版);2004年04期

6 石海鶴;肖正興;薛錦云;;循環(huán)不變式開發(fā)新策略及其應(yīng)用[J];計(jì)算機(jī)工程與應(yīng)用;2006年04期

7 馬竹根;劉槐德;;基于遺傳規(guī)劃尋找循環(huán)不變式的方法[J];計(jì)算機(jī)時(shí)代;2009年02期

8 萬松松;薛錦云;謝武平;;循環(huán)不變式開發(fā)技術(shù)研究[J];計(jì)算機(jī)工程與科學(xué);2010年09期

9 李云清，，薛錦云;利用循環(huán)不變式理解和開發(fā)程序[J];計(jì)算機(jī)與現(xiàn)代化;1996年02期

10 余偉;;循環(huán)不變式在程序設(shè)計(jì)教學(xué)中的應(yīng)用[J];科技風(fēng);2014年14期

相關(guān)博士學(xué)位論文 前2條

1 翟娟;程序驗(yàn)證中的規(guī)約生成與驗(yàn)證技術(shù)研究[D];南京大學(xué);2016年

2 陳石坤;面向程序驗(yàn)證的循環(huán)不變式自動(dòng)構(gòu)造技術(shù)研究[D];國防科學(xué)技術(shù)大學(xué);2010年

相關(guān)碩士學(xué)位論文 前4條

1 萬松松;循環(huán)不變式開發(fā)技術(shù)研究[D];江西師范大學(xué);2008年

2 楊慶紅;遞歸問題循環(huán)不變式開發(fā)新策略的研究與應(yīng)用[D];江西師范大學(xué);2003年

3 劉自恒;循環(huán)不變式生成方法研究與改進(jìn)[D];南京大學(xué);2012年

4 楊黃磊;單元賦值語句型循環(huán)不變式的開發(fā)方法研究[D];江西師范大學(xué);2014年

本文編號：2317217