信息時代的發(fā)展,引領(lǐng)計算機(jī)軟件應(yīng)用深入到千家萬戶,各行各業(yè)。隨著軟件的應(yīng)用領(lǐng)域迅速加大,規(guī)模急速擴(kuò)張,軟件安全性的要求也逐步提升,軟件調(diào)試和維護(hù)的成本越來越高,軟件的安全形勢日漸嚴(yán)峻。基于邏輯推理的形式驗證是提高軟件可信程度的一種重要方法。進(jìn)入21世紀(jì)來,國際國內(nèi)對該方法的推廣和工業(yè)應(yīng)用進(jìn)行了大量的研究與開發(fā),本實驗室（中科大一耶魯高可信軟件聯(lián)合研究中心）在并行程序的驗證方法和串行程序的驗證工具的研發(fā)工作也相當(dāng)活躍。本文工作基于一個類C小語言PointerC的程序驗證器原型。它是研究操作易變數(shù)據(jù)結(jié)構(gòu)的指針程序的驗證的試驗性工具。本文對此驗證器進(jìn)行了兩方面擴(kuò)展,一是使驗證器可以更好地用于一維數(shù)組程序的驗證。二是使驗證器能用于操作帶附加單鏈表的數(shù)據(jù)結(jié)構(gòu)的程序的驗證。本文的主要貢獻(xiàn)如下：第一,設(shè)計并實現(xiàn)了對一維數(shù)組元素進(jìn)行賦值的語句的推理規(guī)則,并將此規(guī)則延伸應(yīng)用到全稱量詞的約束變元出現(xiàn)在訪問路徑的上角標(biāo)中的情況。原型系統(tǒng)雖然主要是針對指針程序設(shè)計的,但同時也考慮了操作其他數(shù)據(jù)類型的程序的驗證,比如操作數(shù)組的程序的驗證。操作一維數(shù)組的程序中,數(shù)組的很多性質(zhì)需要使用量化斷言（如全稱斷言）來描述。... 

【文章來源】：中國科學(xué)技術(shù)大學(xué)安徽省 211工程院校 985工程院校

【文章頁數(shù)】：66 頁

【學(xué)位級別】：碩士

【文章目錄】：
摘要
Abstract
目錄
第1章 緒論
    1.1 研究背景
    1.2 C語言的安全性
    1.3 驗證條件的證明
    1.4 規(guī)范語言的設(shè)計
    1.5 研究工作
    1.6 主要貢獻(xiàn)
第2章 程序驗證器原型簡介
    2.1 PointerC語言
    2.2 形狀分析
    2.3 程序驗證
        2.3.1 Hoare邏輯
        2.3.2 演算規(guī)則
    2.4 原型系統(tǒng)現(xiàn)狀
    2.5 本章小結(jié)
第3章 一維數(shù)組程序的形式驗證
    3.1 Hoare邏輯公理的擴(kuò)展
        3.1.1 Hoare邏輯賦值公理及數(shù)組操作
        3.1.2 擴(kuò)展到一維數(shù)組的賦值公理
        3.1.3 一維數(shù)組元素賦值公理的正向擴(kuò)展
    3.2 全稱斷言的展開規(guī)則
        3.2.1 展開原因
        3.2.2 展開規(guī)則
        3.2.3 整個斷言的展開
    3.3 展開規(guī)則的擴(kuò)展應(yīng)用
    3.4 本章小結(jié)
第4章 操作帶附加單鏈表的數(shù)據(jù)結(jié)構(gòu)程序的形式驗證
    4.1 全局指針變量的處理
        4.1.1 全局指針
        4.1.2 形狀分析中對全局指針變量的處理
    4.2 編程語言的擴(kuò)展
    4.3 形狀分析方法的擴(kuò)展設(shè)計及其正確性證明
    4.4 程序驗證方法的擴(kuò)展
    4.5 本章小結(jié)
第5章 實例分析
    5.1 一維數(shù)組程序
        5.1.1 冒泡排序
        5.1.2 數(shù)組實現(xiàn)二叉堆
    5.2 帶上角標(biāo)全稱斷言的程序
    5.3 操作帶附加單鏈表數(shù)據(jù)結(jié)構(gòu)的程序
    5.4 本章小結(jié)
第6章 總結(jié)及進(jìn)一步工作
    6.1 本文總結(jié)
    6.2 進(jìn)一步研究工作
參考文獻(xiàn)
致謝
在讀期間發(fā)表的學(xué)術(shù)論文與取得的研究成果


【參考文獻(xiàn)】：
期刊論文
[1]指針類型遞歸函數(shù)前后形狀圖的自動推斷[J]. 宋艷輝,李兆鵬,陳意云.  小型微型計算機(jī)系統(tǒng). 2014(04)
[2]一個程序驗證器的設(shè)計和實現(xiàn)[J]. 張志天,李兆鵬,陳意云,劉剛.  計算機(jī)研究與發(fā)展. 2013(05)
[3]循環(huán)不變形狀圖的自動推斷[J]. 劉剛,陳意云,張志天.  電子技術(shù). 2011(08)
[4]一種用于指針程序驗證的指針邏輯[J]. 陳意云,李兆鵬,王志芳,華保健.  軟件學(xué)報. 2010(03)
[5]“可信軟件基礎(chǔ)研究”重大研究計劃綜述[J]. 劉克,單志廣,王戟,何積豐,張兆田,秦玉文.  中國科學(xué)基金. 2008(03)
[6]一種用于指針程序安全性證明的指針邏輯[J]. 陳意云,華保健,葛琳,王志芳.  計算機(jī)學(xué)報. 2008(03)



本文編號：3390282