實(shí)時(shí)系統(tǒng)、嵌入式系統(tǒng)等反應(yīng)式系統(tǒng)（Reactive Systems）往往具有“同步”特性,即模塊間通信時(shí)間可忽略不計(jì),同一時(shí)刻多個(gè)信號(hào)可同時(shí)發(fā)生.同步系統(tǒng)模型作為同步編程語(yǔ)言（如Esterel、Signal等）的基礎(chǔ),被廣泛應(yīng)用于反應(yīng)式系統(tǒng),特別是嵌入式系統(tǒng)的建模中.隨著近年來(lái)物聯(lián)網(wǎng)、信息物理系統(tǒng)等分布式實(shí)時(shí)嵌入式系統(tǒng)的蓬勃發(fā)展,同步系統(tǒng)的建模、規(guī)約與驗(yàn)證變得愈發(fā)重要.在同步系統(tǒng)中,基于“時(shí)鐘約束”的系統(tǒng)規(guī)約在系統(tǒng)的安全性和可靠性方面扮演著關(guān)鍵角色.時(shí)鐘約束規(guī)約語(yǔ)言（Clock Constraint Specification Language,簡(jiǎn)稱(chēng)CCSL）是一種基于“時(shí)鐘”和時(shí)鐘約束關(guān)系的形式化規(guī)約語(yǔ)言.它被廣泛地應(yīng)用于同步系統(tǒng)的規(guī)約與驗(yàn)證.以往CCSL規(guī)約的驗(yàn)證技術(shù)主要基于模型檢測(cè).由于模型檢測(cè)技術(shù)的局限性,這些驗(yàn)證技術(shù)不支持無(wú)限狀態(tài)CCSL規(guī)約（亦稱(chēng)為“非安全”CCSL規(guī)約）的驗(yàn)證.對(duì)于狀態(tài)空間較大的系統(tǒng),基于模型檢測(cè)的驗(yàn)證技術(shù)存在狀態(tài)空間爆炸的問(wèn)題.動(dòng)態(tài)邏輯（Dynamic Logic,簡(jiǎn)稱(chēng)DL）是一種對(duì)程序動(dòng)態(tài)行為進(jìn)行刻畫(huà)和推理的模態(tài)邏輯,其驗(yàn)證技術(shù)主要基于定理證明和SMT... 

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

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

【文章目錄】：
摘要
ABSTRACT
第一章 緒論
    1.1 研究背景與現(xiàn)狀
        1.1.1 同步系統(tǒng)模型
        1.1.2 CCSL
        1.1.3 動(dòng)態(tài)邏輯
        1.1.4 本文關(guān)注的研究問(wèn)題
    1.2 研究問(wèn)題
    1.3 主要貢獻(xiàn)
        1.3.1 研究思路
        1.3.2 研究意義
        1.3.3 主要工作
    1.4 章節(jié)安排
第二章 預(yù)備知識(shí)
    2.1 CCSL語(yǔ)言
    2.2 Kripke框架
    2.3 一階動(dòng)態(tài)邏輯FODL
    2.4 Sequent演算
    2.5 本章小結(jié)
第三章 面向順序程序的時(shí)鐘約束動(dòng)態(tài)邏輯sCDL
    3.1 引言
    3.2 同步事件順序程序SESP
    3.3 sCDL公式的語(yǔ)法
    3.4 sCDL邏輯的語(yǔ)義
        3.4.1 sCDL邏輯的解釋,Kripke框架和賦值
        3.4.2 SESP程序的語(yǔ)義
        3.4.3 sCDL公式的語(yǔ)義
        3.4.4 可滿(mǎn)足關(guān)系和替換定理
    3.5 sCDL邏輯證明系統(tǒng)
        3.5.1 路徑公式規(guī)則
        3.5.2 非路徑公式的規(guī)則
        3.5.3 其它邏輯規(guī)則
    3.6 一個(gè)sCDL邏輯的案例分析
        3.6.1 Feeder系統(tǒng)
        3.6.2 sCDL邏輯的局限性
    3.7 本章小結(jié)
第四章 時(shí)鐘約束動(dòng)態(tài)邏輯CDL
    4.1 引言
    4.2 CDL公式的語(yǔ)法
        4.2.1 同步事件程序SEP
        4.2.2 CDL公式的語(yǔ)法
    4.3 CDL公式的語(yǔ)義
        4.3.1 SEP程序的邏輯一致性
        4.3.2 并行交互條件邏輯公式的構(gòu)造與并行trec程序的語(yǔ)義
        4.3.3 SEP程序的語(yǔ)義
        4.3.4 CDL上的可滿(mǎn)足關(guān)系與替換定理
    4.4 CDL邏輯證明系統(tǒng)
        4.4.1 CDL邏輯并行算子的規(guī)則
        4.4.2 并行算子證明規(guī)則中的算法
        4.4.3 SEP程序的可推導(dǎo)關(guān)系
    4.5 CCSL規(guī)約在時(shí)鐘約束動(dòng)態(tài)邏輯中的表示
    4.6 本章小結(jié)
第五章 CDL邏輯系統(tǒng)的分析
    5.1 引言
    5.2 CDL邏輯證明系統(tǒng)的可靠性
        5.2.1 非并行算子證明規(guī)則的可靠性
        5.2.2 并行算子證明規(guī)則的可靠性
    5.3 CDL邏輯證明系統(tǒng)的相對(duì)完備性
        5.3.1 相對(duì)完備性定理的證明
        5.3.2 相對(duì)完備性定理中各條件的證明
    5.4 本章小結(jié)
第六章 CDL邏輯系統(tǒng)的案例分析
    6.1 引言
    6.2 數(shù)字濾波器系統(tǒng)
        6.2.1 系統(tǒng)功能介紹
        6.2.2 系統(tǒng)行為、性質(zhì)的建模
    6.3 車(chē)載自動(dòng)窗系統(tǒng)
        6.3.1 系統(tǒng)功能介紹
        6.3.2 系統(tǒng)行為、性質(zhì)的建模
    6.4 系統(tǒng)CCSL規(guī)約在CDL邏輯系統(tǒng)中的證明
    6.5 本章小結(jié)
第七章 總結(jié)和展望
    7.1 本文工作總結(jié)
    7.2 未來(lái)工作的展望
參考文獻(xiàn)
致謝
攻讀博士學(xué)位期間發(fā)表論文和科研情況


【參考文獻(xiàn)】：
期刊論文
[1]信息物理融合系統(tǒng)研究[J]. 李馥娟,王群,錢(qián)煥延.  電子技術(shù)應(yīng)用. 2018(09)
[2]信息物理融合系統(tǒng)研究綜述[J]. 王中杰,謝璐璐.  自動(dòng)化學(xué)報(bào). 2011(10)
[3]物聯(lián)網(wǎng)技術(shù)研究綜述[J]. 王保云.  電子測(cè)量與儀器學(xué)報(bào). 2009(12)
[4]模型檢測(cè):理論、方法與應(yīng)用[J]. 林惠民,張文輝.  電子學(xué)報(bào). 2002(S1)



本文編號(hào)：3712701