如何對安全關(guān)鍵混成系統(tǒng)進行形式化建模及驗證方法是一項重要的科學(xué)問題。在現(xiàn)有的工程實踐中,作為驗證對象的安全屬性缺乏規(guī)范化的獲取方式;工業(yè)應(yīng)用廣泛的形式化建模語言LUSTRE不支持對物理世界連續(xù)行為的建模;系統(tǒng)的高復(fù)雜度帶來的狀態(tài)空間爆炸問題使得驗證無法完成。這些難點的存在阻礙著安全關(guān)鍵混成系統(tǒng)的安全性的進一步提高,已經(jīng)成為了安全關(guān)鍵軟件行業(yè)不可回避的挑戰(zhàn)。本文以構(gòu)建安全關(guān)鍵混成系統(tǒng)建模與驗證方法為研究目標,從分析需求規(guī)約出發(fā),針對形式化驗證方法中模型檢驗方法的特征,提出了一套可行的規(guī)范化流程,主要貢獻包括:·提出了安全關(guān)鍵混成系統(tǒng)建模及驗證框架。該框架從需求規(guī)約出發(fā),覆蓋了對系統(tǒng)進行需求建模、需求分解、設(shè)計建模、驗證實現(xiàn)等步驟,解決了從需求出發(fā)難以構(gòu)建對系統(tǒng)進行驗證所需的組件的問題。·提出了兩種基于投影的問題分解方法。這兩種方法都以問題框架方法為基礎(chǔ),分別從子需求和變量約束的角度尋找投影維度,對問題模型進行分解。從而降低了描述安全關(guān)鍵混成系統(tǒng)的問題的復(fù)雜度。·定義了混成系統(tǒng)建模語言Hybrid LUSTRE。該語言以同步建模語言LUS-TRE為基礎(chǔ),結(jié)合混成自動機時間模型,給出了形式化...

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

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

【文章目錄】：
內(nèi)容摘要
Abstract
第一章 引言
    1.1 研究背景
    1.2 研究現(xiàn)狀
        1.2.1 混成系統(tǒng)建模方法
        1.2.2 混成系統(tǒng)驗證方法
    1.3 本文工作
    1.4 論文結(jié)構(gòu)
第二章 工作基礎(chǔ)
    2.1 混成系統(tǒng)
    2.2 模型檢驗
    2.3 同步建模語言LUSTRE
    2.4 問題框架方法
    2.5 本章小結(jié)
第三章 安全關(guān)鍵混成系統(tǒng)建模及驗證框架
    3.1 框架概述
    3.2 建模方法
    3.3 驗證系統(tǒng)建模方法
    3.4 本章小結(jié)
第四章 需求建模和需求分解
    4.1 需求建模
    4.2 基于子需求的問題分解方法
    4.3 基于約束的問題分解方法
        4.3.1 約束分類
        4.3.2 投影維度的選擇
        4.3.3 基于約束的投影的定義
    4.4 本章小結(jié)
第五章 混成系統(tǒng)同步建模語言Hybrid LUSTRE
    5.1 語言設(shè)計
    5.2 Hybrid LUSTRE語法
        5.2.1 表達式
        5.2.2 節(jié)點
    5.3 Hybrid LUSTRE語義
        5.3.1 指稱語義
        5.3.2 安全語義
        5.3.3 活性語義
    5.4 設(shè)計建模及實現(xiàn)
    5.5 本章小結(jié)
第六章 驗證問題的需求建模到設(shè)計建模
    6.1 驗證問題的需求建模
    6.2 驗證問題的需求分解
        6.2.1 假設(shè)與理論依據(jù)
        6.2.2 基于子安全屬性的驗證問題分解
        6.2.3 基于約束的驗證問題分解
    6.3 驗證問題的設(shè)計建模及實現(xiàn)
    6.4 本章小結(jié)
第七章 基于通信的列車控制系統(tǒng)的建模與驗證
    7.1 案例描述
    7.2 工具支持
    7.3 需求建模
        7.3.1 需求描述
        7.3.2 需求問題
    7.4 需求分解
        7.4.1 基于子屬性的建模問題分解
        7.4.2 基于約束的建模問題分解
    7.5 設(shè)計建模及實現(xiàn)
        7.5.1 設(shè)計建模
        7.5.2 模型實現(xiàn)
    7.6 驗證問題的建模與驗證
        7.6.1 驗證需求獲取
        7.6.2 驗證問題需求建模
        7.6.3 驗證問題需求分解
    7.7 驗證結(jié)果與評估
        7.7.1 驗證耗時對比
        7.7.2 適用系統(tǒng)規(guī)模
        7.7.3 兩種問題分解方法的對比
    7.8 本章小結(jié)
第八章 總結(jié)與展望
附錄
參考文獻
致謝
攻讀博士學(xué)位期間發(fā)表論文和科研情況



本文編號：3888899