進(jìn)入21世紀(jì)以來(lái),信息技術(shù)已逐漸成為推動(dòng)經(jīng)濟(jì)發(fā)展和提升生產(chǎn)效率的強(qiáng)大動(dòng)力,軟件技術(shù)的普及度越來(lái)越高,軟件行業(yè)呈現(xiàn)出高速發(fā)展的趨勢(shì)。隨著計(jì)算機(jī)系統(tǒng)規(guī)模日益增加、問(wèn)題域不斷加大,其系統(tǒng)設(shè)計(jì)的復(fù)雜度也在不斷飆升。系統(tǒng)復(fù)雜度的增加意味著出現(xiàn)錯(cuò)誤的可能性也就更大,其安全性不容忽視;如何保障程序的安全性和提高程序的可靠性一直以來(lái)是軟件技術(shù)發(fā)展的核心問(wèn)題之一。以窮舉狀態(tài)為基礎(chǔ)的模型檢測(cè)因其自動(dòng)化程度高,并能在系統(tǒng)不滿足性質(zhì)時(shí)提供反例等優(yōu)點(diǎn)受到普遍關(guān)注和應(yīng)用,成為解決該問(wèn)題的有效途徑之一。由于現(xiàn)有模型檢測(cè)工具的形式化規(guī)范語(yǔ)言,如計(jì)算樹(shù)邏輯（computation tree logic,簡(jiǎn)稱CTL）和線性時(shí)序邏輯（linear temporal logic,簡(jiǎn)稱LTL）等,存在規(guī)范描述能力不足,無(wú)法驗(yàn)證實(shí)時(shí)時(shí)序邏輯（real-time temporal logic,簡(jiǎn)稱RTCTL*）的問(wèn)題,本文基于全時(shí)序測(cè)試器（簡(jiǎn)稱測(cè)試器）優(yōu)化了 RTCTL*算法并證明了關(guān)鍵測(cè)試器的正確性和完備性,提出了一種RTCTL*符號(hào)模型檢測(cè)工具——RTSMC（RTCTL*symbolic model checker）,該工具基... 

【文章來(lái)源】：華僑大學(xué)福建省

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

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

【文章目錄】：
摘要
Abstract
第1章 引言
    1.1 研究背景與意義
    1.2 國(guó)內(nèi)外研究現(xiàn)狀
    1.3 論文的主要工作
    1.4 論文結(jié)構(gòu)
    1.5 本章小結(jié)
第2章 相關(guān)技術(shù)
    2.1 形式化驗(yàn)證
    2.2 ROBDD
    2.3 JAVABDD
    2.4 符號(hào)化模型檢測(cè)
    2.5 規(guī)范
    2.6 模型檢測(cè)工具
    2.7 本章小結(jié)
第3章 基于全測(cè)試器的符號(hào)模型檢測(cè)算法
    3.1 基礎(chǔ)模型
        3.1.1 公平性離散系統(tǒng)JDS
        3.1.2 JDS的同步并行組合
        3.1.3 RTCTL* 語(yǔ)法語(yǔ)義及等價(jià)關(guān)系
        3.1.4 測(cè)試器——“全時(shí)序測(cè)試器”的簡(jiǎn)稱
    3.2 RTCTL* 算法與證明
        3.2.1 RTCTL* 的測(cè)試器
        3.2.2 ?f的測(cè)試器
        3.2.3 f ∧ g的測(cè)試器
        3.2.4 Ef的測(cè)試器
        3.2.5 Xf的測(cè)試器及證明
        3.2.6 fUg的測(cè)試器及證明
        3.2.7 fU[a,b]g的測(cè)試器及證明
    3.3 本章小結(jié)
第4章 基于JTLV實(shí)現(xiàn)RTSMC
    4.1 系統(tǒng)原型框架
    4.2 RTSMC驗(yàn)證流程
    4.3 詞法語(yǔ)法解析
    4.4 RTSMC核心模塊的實(shí)現(xiàn)
        4.4.1 RTCTL* 接口
        4.4.2 Env擴(kuò)展
        4.4.3 RTCTL* 構(gòu)造器
        4.4.4 RTCTL* 解析器
    4.5 本章小結(jié)
第5章 實(shí)驗(yàn)結(jié)果與分析
    5.1 實(shí)驗(yàn)環(huán)境
    5.2 實(shí)驗(yàn)結(jié)果展示與分析
        5.2.1 功能 & 邊界測(cè)試
        5.2.2 對(duì)比Nu SMV驗(yàn)證實(shí)時(shí)時(shí)序邏輯
        5.2.3 對(duì)比nu XMV驗(yàn)證實(shí)時(shí)時(shí)序邏輯
    5.3 本章小結(jié)
第6章 總結(jié)與展望
    6.1 本文的主要成果
    6.2 本文的創(chuàng)新點(diǎn)
    6.3 本文的不足
    6.4 后續(xù)工作展望
參考文獻(xiàn)
致謝



本文編號(hào)：2936839