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

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

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

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



本文編號(hào)：3888899