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

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

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

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

【文章目錄】：
摘要
Abstract
目錄
第1章 緒論
    1.1 研究背景
    1.2 C語言的安全性
    1.3 驗(yàn)證條件的證明
    1.4 規(guī)范語言的設(shè)計(jì)
    1.5 研究工作
    1.6 主要貢獻(xiàn)
第2章 程序驗(yàn)證器原型簡介
    2.1 PointerC語言
    2.2 形狀分析
    2.3 程序驗(yàn)證
        2.3.1 Hoare邏輯
        2.3.2 演算規(guī)則
    2.4 原型系統(tǒng)現(xiàn)狀
    2.5 本章小結(jié)
第3章 一維數(shù)組程序的形式驗(yàn)證
    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 整個(gè)斷言的展開
    3.3 展開規(guī)則的擴(kuò)展應(yīng)用
    3.4 本章小結(jié)
第4章 操作帶附加單鏈表的數(shù)據(jù)結(jié)構(gòu)程序的形式驗(yàn)證
    4.1 全局指針變量的處理
        4.1.1 全局指針
        4.1.2 形狀分析中對(duì)全局指針變量的處理
    4.2 編程語言的擴(kuò)展
    4.3 形狀分析方法的擴(kuò)展設(shè)計(jì)及其正確性證明
    4.4 程序驗(yàn)證方法的擴(kuò)展
    4.5 本章小結(jié)
第5章 實(shí)例分析
    5.1 一維數(shù)組程序
        5.1.1 冒泡排序
        5.1.2 數(shù)組實(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ù)前后形狀圖的自動(dòng)推斷[J]. 宋艷輝,李兆鵬,陳意云.  小型微型計(jì)算機(jī)系統(tǒng). 2014(04)
[2]一個(gè)程序驗(yàn)證器的設(shè)計(jì)和實(shí)現(xiàn)[J]. 張志天,李兆鵬,陳意云,劉剛.  計(jì)算機(jī)研究與發(fā)展. 2013(05)
[3]循環(huán)不變形狀圖的自動(dòng)推斷[J]. 劉剛,陳意云,張志天.  電子技術(shù). 2011(08)
[4]一種用于指針程序驗(yàn)證的指針邏輯[J]. 陳意云,李兆鵬,王志芳,華保健.  軟件學(xué)報(bào). 2010(03)
[5]“可信軟件基礎(chǔ)研究”重大研究計(jì)劃綜述[J]. 劉克,單志廣,王戟,何積豐,張兆田,秦玉文.  中國科學(xué)基金. 2008(03)
[6]一種用于指針程序安全性證明的指針邏輯[J]. 陳意云,華保健,葛琳,王志芳.  計(jì)算機(jī)學(xué)報(bào). 2008(03)



本文編號(hào)：3390282