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

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

【學位級別】：碩士

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



本文編號：3649554