隨著軟件規(guī)模越來(lái)越大,軟件安全性越來(lái)越引起開(kāi)發(fā)人員的關(guān)注,而現(xiàn)有的編程語(yǔ)言以及軟件開(kāi)發(fā)方法所能提供的安全性保證是脆弱和不可靠的,例如,通過(guò)標(biāo)準(zhǔn)的軟件工程方法和大量的測(cè)試能夠減少軟件漏洞產(chǎn)生,但是即使經(jīng)過(guò)高強(qiáng)度測(cè)試的軟件,我們也不能保證其沒(méi)有漏洞,并且這些方法不具有可再現(xiàn)性。已有的軟件工程方法對(duì)軟件安全性的提高已經(jīng)越來(lái)越微弱,而基于Hoare邏輯的程序形式化驗(yàn)證方法能為軟件安全性提供可靠保證。本文針對(duì)目前程序驗(yàn)證的不可再現(xiàn)性,基于Hoare邏輯中最強(qiáng)后置條件謂詞轉(zhuǎn)換,給出了一些可重現(xiàn)的形式化技術(shù)和方法求解代碼語(yǔ)義,其解決了程序驗(yàn)證的可應(yīng)用性與可重現(xiàn)性。首先,通過(guò)分析推導(dǎo)程序語(yǔ)義的形式化方法,討論在求解賦值語(yǔ)句最強(qiáng)后置條件中存在的自動(dòng)化方面的問(wèn)題。給出賦值語(yǔ)句最強(qiáng)后置條件的一個(gè)新定義,使用這個(gè)定義即不需求解反函數(shù),也無(wú)需引入一個(gè)新變量就能自動(dòng)化地求解賦值語(yǔ)句的最強(qiáng)后置條件。其次,針對(duì)求解循環(huán)程序語(yǔ)義時(shí)需事先知道循環(huán)深度這一缺陷,給出了一種求解命令式循環(huán)程序語(yǔ)義及其執(zhí)行和終止條件的方法。該方法包括直接從代碼本身進(jìn)行循環(huán)執(zhí)行和終止條件的算法推導(dǎo),并可將推出的循環(huán)語(yǔ)義信息應(yīng)用到程序驗(yàn)證和缺陷修正... 

【文章頁(yè)數(shù)】：75 頁(yè)

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

【文章目錄】：
摘要
Abstract
第一章緒論
    1.1 研究背景
    1.2 論文的應(yīng)用價(jià)值
    1.3 論文的組織結(jié)構(gòu)
第二章 相關(guān)技術(shù)分析
    2.1 Hoare 邏輯
        2.1.1 邏輯正確性概念
        2.1.2 部分正確性證明規(guī)則
    2.2 形式化符號(hào)表示
        2.2.1 項(xiàng)及公式
        2.2.2 函數(shù)
        2.2.3 其他符號(hào)約定
    2.3 確認(rèn)與驗(yàn)證
        2.3.1 形式化驗(yàn)證方法
        2.3.2 軟件測(cè)試
        2.3.3 軟件審查
    2.4 最強(qiáng)后置條件謂詞轉(zhuǎn)換
        2.4.1 賦值語(yǔ)句的最強(qiáng)后置條件
        2.4.2 順序結(jié)構(gòu)的最強(qiáng)后置條件
        2.4.3 分支結(jié)構(gòu)的最強(qiáng)后置條件
        2.4.4 迭代結(jié)構(gòu)的最強(qiáng)后置條件
        2.4.5 過(guò)程調(diào)用的最強(qiáng)后置條件
        2.4.6 變量聲明的最強(qiáng)后置條件
    2.5 本章小節(jié)
第三章 基于Hoare 邏輯的循環(huán)程序驗(yàn)證技術(shù)研究
    3.1 引言
    3.2 迭代不變式
        3.2.1 差分方程
        3.2.2 迭代相關(guān)性的表示方法
        3.2.3 求解迭代不變式
    3.3 循環(huán)執(zhí)行條件的研究
        3.3.1 簡(jiǎn)單循環(huán)條件
        3.3.2 復(fù)雜循環(huán)條件
    3.4 循環(huán)終止條件研究
    3.5 本章小節(jié)
第四章 基于Hoare 邏輯的過(guò)程驗(yàn)證技術(shù)研究
    4.1 引言
    4.2 過(guò)程和過(guò)程調(diào)用規(guī)則
    4.3 提取過(guò)程語(yǔ)義
    4.4 過(guò)程調(diào)用的語(yǔ)義
        4.4.1 參數(shù)代換
        4.4.2 檢驗(yàn)過(guò)程的前置條件
        4.4.3 過(guò)程調(diào)用的最強(qiáng)后置條件
    4.5 Hoare 邏輯在函數(shù)驗(yàn)證中的應(yīng)用
    4.6 本章小節(jié)
第五章 基于Hoare 邏輯的程序驗(yàn)證技術(shù)的應(yīng)用
    5.1 引言
    5.2 公理證明法
        5.2.1 使用R_(k+1) 證明程序部分正確性
        5.2.2 識(shí)別不一致性
        5.2.3 直接證明方法
    5.3 基于功能理論的正確性證明方法
    5.4 本章小節(jié)
第六章 總結(jié)與展望
    6.1 本文的工作總結(jié)
    6.2 下一步工作展望
參考文獻(xiàn)
作者簡(jiǎn)歷 攻讀碩士學(xué)位期間完成的主要工作
致謝



本文編號(hào)：3649554