本文選題：程序驗證 + 規(guī)約��； 參考：《南京大學》2016年博士論文

【摘要】：隨著計算機科學與技術的迅速發(fā)展,軟件的規(guī)模越來越大,軟件的可靠性越來越難以保障,如何保障軟件的正確性是計算機科學的一個巨大的挑戰(zhàn)。程序驗證是保障軟件正確性、提高軟件可信度的可靠方法,其中定理證明這一方法利用邏輯和數(shù)學手段,通過演繹推理來驗證軟件的正確性,這種方法可以極大地提高人們對軟件的信心,是近年來的研究熱點。定理證明的基本思想是通過某種斷言描述程序的形式規(guī)約,根據(jù)斷言對程序進行邏輯演算生成驗證條件,借助定理證明工具證明驗證條件的正確性,從而證明程序的正確性,保障軟件的可信性。但是,提供合適的規(guī)約要求驗證人員對程序有深刻的理解,對于驗證人員來說是一件非常困難的事情,因此,自動生成程序規(guī)約是程序驗證領域中的重要研究內(nèi)容,其中關于循環(huán)語句以及類庫的研究是重中之重。循環(huán)語句廣泛存在于各類程序中,循環(huán)語句的規(guī)約在程序驗證領域中具有不可替代的作用,循環(huán)語句規(guī)約的自動生成與驗證中的難點主要在于循環(huán)不變式的自動生成與檢驗,然而循環(huán)語句復雜多樣,不存在統(tǒng)一的方法可以為所有的循環(huán)自動生成規(guī)約。現(xiàn)在的軟件程序大量依賴于類庫,類庫的行為已經(jīng)成為軟件行為中不可分割的一部分,類庫的規(guī)約在很多程序分析驗證技術中扮演著不可或缺的重要角色,是很多程序分析過程的前提條件。然而類庫的源代碼通常規(guī)模龐大、邏輯復雜,有時甚至根本無法獲取,因此,生成類庫的規(guī)約異常困難。本文針對規(guī)約的自動生成與驗證問題展開研究,主要工作包括以下幾個方面：1.提出了一種綜合考慮程序代碼和程序規(guī)約來構造循環(huán)不變式的方法,即基于循環(huán)語句已有的斷言生成循環(huán)不變式。首先通過將循環(huán)語句的后置條件以及循環(huán)體的斷言通過子表達式替換、添加全稱量詞和尋找遞推關系的方式來生成候選的循環(huán)不變式,然后對每一個候選的循環(huán)不變式,借助定理證明器和最弱前置條件的計算來證明候選循環(huán)不變式的正確性以及相關斷言的正確性。本文提出的方法所生成的循環(huán)不變式既可以描述數(shù)據(jù)結構的形狀性質(zhì),也可以描述數(shù)據(jù)結構所存儲的元素之間的關系以及元素與標量變量、常量之間的關系。該方法已經(jīng)實現(xiàn)并集成到程序驗證工具中,實驗數(shù)據(jù)表明,本文提出的方法可以有效地為操作常用數(shù)據(jù)結構的循環(huán)自動生成循環(huán)不變式,提高程序驗證的自動化程度和效率,減輕驗證人員的負擔。2.定義了一種描述程序語句摘要的方法,將摘要定義為語句修改的內(nèi)存以及語句執(zhí)行結束以后這些內(nèi)存中存放的新值�；谘h(huán)語句的摘要,循環(huán)語句可以被轉(zhuǎn)換為一系列抽象的賦值語句,從而可以將帶有循環(huán)語句的程序轉(zhuǎn)換為不包含循環(huán)的程序,從而可以使用分析賦值語句的方法來分析循環(huán)語句。提出了自動生成程序語句的摘要的方法,可以有效地為賦值語句、順序語句、條件語句以及操作常用數(shù)據(jù)結構的循環(huán)語句自動生成摘要,其中循環(huán)語句可以嵌套多層循環(huán)和分支結構。同時提出了一種根據(jù)語句的摘要自動生成程序語句的規(guī)約的方法,生成的規(guī)約類型包括后置條件、前置條件以及循環(huán)不變式。該方法已經(jīng)實現(xiàn)并集成到程序驗證工具中,生成語句摘要的方法所需要的時間和循環(huán)的個數(shù)成線性關系,相比于以往借助于抽象解釋等對循環(huán)語句進行分析的方法,我們的方法效率更高。根據(jù)摘要所生成的規(guī)約可以有效地輔助程序的形式化驗證過程,既可以減輕程序驗證人員人工提供程序規(guī)約的負擔同時又可以提高驗證程序的效率。3.提出了一種基于文檔自動生成類庫的代碼模型的方法,該方法綜合使用了自然語言處理技術和自動化測試技術。所生成的模型模擬了類庫的行為,但是模型的代碼實現(xiàn)更加簡單,從而解決了因為類庫源代碼缺失導致無法分析的問題以及分析復雜的類庫源代碼非常困難的問題。有了類庫的代碼模型,就可以通過對模型進行分析來生成類庫的規(guī)約,用于證明程序的正確性。開發(fā)完成的工具原型可以為Java類庫中14個常用類和2個常用接口的326個庫函數(shù)自動生成代碼模型,并將生成的代碼模型應用于類庫的規(guī)約生成、Android污點分析和Java動態(tài)切片中。在類庫的規(guī)約生成中,通過對代碼模型的分析可以自動生成類庫函數(shù)的外部規(guī)約,通過對外部規(guī)約進行實例化可以生成調(diào)用類庫函數(shù)的程序的規(guī)約。在Android污點分析中,使用代碼模型可以發(fā)現(xiàn)一些使用類庫源代碼無法發(fā)現(xiàn)的信息泄露路徑,而且使用代碼模型進行分析時,效率上也有所提升。在Java動態(tài)切片中,使用代碼模型比使用樸素模型所生成的切片更精確而且效率更高。總體結果表明我們的方法可以準確地為類庫的行為進行建模,有效地為類庫的函數(shù)生成規(guī)約,并且提高其它程序分析技術的有效性和效率。
[Abstract]:With the rapid development of computer science and technology , the scale of software becomes more and more difficult , and the reliability of software is more and more difficult to guarantee . This paper presents a method for automatically generating code model of class library by analyzing the code model .

【學位授予單位】：南京大學
【學位級別】：博士
【學位授予年份】：2016
【分類號】：TP311.53

【相似文獻】

相關期刊論文 前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)不變式自動構造技術研究[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年

本文編號：1867354