【摘要】：采用形式化方法證明軟件的正確性,是保障軟件可靠性的有效方法.而對循環(huán)語句的分析與驗證,是形式化證明中的關鍵,對循環(huán)語句的處理一直是程序分析與驗證中的一個難點問題.提出使用循環(huán)語句修改的內(nèi)存和這些內(nèi)存中存放的新值來描述循環(huán)語句的執(zhí)行效果,并將該執(zhí)行效果定義為循環(huán)摘要.同時,提出一種自動生成循環(huán)摘要的方法,可以為操作常用數(shù)據(jù)結(jié)構(gòu)的循環(huán)自動生成循環(huán)摘要,包含嵌套循環(huán).此外,基于循環(huán)摘要,可以自動生成循環(huán)語句的規(guī)約,包括循環(huán)不變式、循環(huán)的前置條件以及循環(huán)的后置條件.已經(jīng)實現(xiàn)了自動生成循環(huán)摘要以及循環(huán)規(guī)約的方法,并將它們集成到驗證工具Accumulator中.實驗結(jié)果表明,該方法可以有效地生成循環(huán)摘要,并生成多種類型的規(guī)約,從而輔助軟件程序的形式化證明,提高驗證的自動化程度和效率,減輕驗證人員的負擔.
[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.
【作者單位】： 計算機軟件新技術國家重點實驗室(南京大學);南京大學軟件學院;南京大學計算機科學與技術系;
【基金】：國家自然科學基金(61632015,61561146394) 國家重點研發(fā)計劃(2016YFB1000802)~~
【分類號】：TP311

【參考文獻】

相關期刊論文 前6條

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

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

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

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

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

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

【相似文獻】

相關期刊論文 前10條

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

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

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

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

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

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

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

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

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

10 余偉;;循環(huán)不變式在程序設計教學中的應用[J];科技風;2014年14期

相關博士學位論文 前2條

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

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

相關碩士學位論文 前4條

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

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

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

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

本文編號：2317217