發(fā)布時間：2023-06-28 03:50

　　在智能時代,隨著信息系統(tǒng)的規(guī)模和復(fù)雜度日益增大,人們對系統(tǒng)運行時的安全性和可靠性的要求越來越高。限界模型檢測技術(shù)作為自動檢驗系統(tǒng)的有效手段,在提高系統(tǒng)可信性上發(fā)揮著重要作用。限界模型檢測與插值序列相結(jié)合可以完成限定邊界外屬性的驗證,進而實現(xiàn)無界模型檢測。然而,插值序列的引入會增大模型編碼的復(fù)雜程度,影響模型檢測器整體的性能。針對這個問題,本文提出了基于插值的多核限界模型檢測方法。本文的主要工作和創(chuàng)新點如下:首先,本文提出基于插值和狀態(tài)空間劃分的屬性驗證算法,將問題分解并利用多核技術(shù)并行求解。模型狀態(tài)空間中的狀態(tài)遷移路徑被劃分為路徑簇,再利用限界模型檢測和基于插值序列的可達性分析方法對路徑簇進行驗證。其次,利用路徑簇中存在不動點的性質(zhì),本文提出路徑簇剪枝算法,縮小待搜索狀態(tài)空間的規(guī)模以提高檢測效率。最后,為了進一步改進算法,本文提出了增量編碼和驗證假設(shè)兩種優(yōu)化方法。增量編碼的思想是定量增加檢測限界,減少約束求解器的調(diào)用次數(shù)。驗證假設(shè)的思想是在模型檢測中利用驗證歷史信息,將已驗證過的屬性加入到命題公式中,提高插值的求解效率。本文提出的基于插值的多核限界模型檢測方法應(yīng)用于層次狀態(tài)變遷矩陣描述...

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

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

【文章目錄】：
摘要
Abstract
1 緒論
    1.1 研究背景
    1.2 國內(nèi)外研究現(xiàn)狀
        1.2.1 模型檢測方法
        1.2.2 插值驗證方法
    1.3 研究內(nèi)容
    1.4 論文結(jié)構(gòu)
2 相關(guān)理論背景
    2.1 限界模型檢測
    2.2 層次狀態(tài)變遷矩陣
    2.3 線性時序邏輯
    2.4 插值定理
    2.5 本章小結(jié)
3 基于插值的多核限界模型檢測算法
    3.1 主要思想
    3.2 限界模型檢測
        3.2.1 限界增量編碼
        3.2.2 狀態(tài)空間搜索
    3.3 基于插值的分析
    3.4 模型分簇
        3.4.1 路徑簇劃分
        3.4.2 多核檢測
    3.5 本章小結(jié)
4 面向活性屬性的檢測方法
    4.1 套索檢測
    4.2 活性屬性轉(zhuǎn)化
    4.3 模型編碼與驗證
    4.4 本章小結(jié)
5 驗證與實驗結(jié)果分析
    5.1 實驗環(huán)境與工具
    5.2 實驗方案概述
    5.3 實驗結(jié)果分析
        5.3.1 基于插值的模型檢測實驗
        5.3.2 限界增量檢測對比實驗
        5.3.3 多核模型檢測實驗
        5.3.4 活性屬性實驗
    5.4 本章小結(jié)
結(jié)論
參考文獻
攻讀碩士學(xué)位期間發(fā)表學(xué)術(shù)論文情況
致謝



本文編號：3835923