發(fā)布時(shí)間：2024-03-17 09:43

　　信息物理融合系統(tǒng)(Cyber-Physical System, CPS)基于計(jì)算機(jī)互聯(lián)網(wǎng),在物與物互聯(lián)的基礎(chǔ)上,將計(jì)算(computation)、通信(communication)、控制(control)3C技術(shù)融合在一起,強(qiáng)調(diào)對(duì)物實(shí)時(shí)、動(dòng)態(tài)的信息控制與信息服務(wù),是國(guó)內(nèi)外信息技術(shù)領(lǐng)域研究的一類(lèi)重要系統(tǒng)。如何對(duì)CPS系統(tǒng)進(jìn)行建模,以及驗(yàn)證模型中的性質(zhì)以確保CPS系統(tǒng)的保真性、可靠性等特點(diǎn)是一個(gè)重要的研究問(wèn)題。 本文主要采用微分動(dòng)態(tài)邏輯(Differential Dynamic Logic, dL)、結(jié)構(gòu)分析與設(shè)計(jì)語(yǔ)言(Architecture Analysis and Design Language, AADL)和時(shí)鐘理論(Clock Theory)分別對(duì)不同的CPS應(yīng)用場(chǎng)景進(jìn)行建模分析并驗(yàn)證了其安全性性質(zhì)。 利用微分動(dòng)態(tài)邏輯對(duì)CPS系統(tǒng)鐵路道口控制進(jìn)行形式化建模與分析。從火車(chē)發(fā)送接近信號(hào)到進(jìn)入道口的運(yùn)動(dòng)過(guò)程中,針對(duì)火車(chē)到達(dá)道口的時(shí)間要求,將火車(chē)速度控制問(wèn)題抽象成一個(gè)混成系統(tǒng)的安全性性質(zhì),用微分動(dòng)態(tài)邏輯來(lái)描述,并使用混成系統(tǒng)證明工具KeYmaera對(duì)系統(tǒng)的安全性進(jìn)行了驗(yàn)證,實(shí)現(xiàn)對(duì)火車(chē)進(jìn)入...

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

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

【文章目錄】：
摘要
Abstract
第一章 緒論
    1.1 研究背景
        1.1.1 物聯(lián)網(wǎng)和信息物理融合系統(tǒng)
        1.1.2 混成系統(tǒng)
            1.1.2.1 混成系統(tǒng)定義
            1.1.2.2 混成系統(tǒng)案例
    1.2 國(guó)內(nèi)外研究現(xiàn)狀
    1.3 研究?jī)?nèi)容和方法
    1.4 文章結(jié)構(gòu)
    1.5 本章小結(jié)
第二章 微分動(dòng)態(tài)邏輯對(duì)CPS的建模
    2.1 概述
    2.2 混成程序
        2.2.1 混成程序介紹
        2.2.2 混成程序的語(yǔ)法語(yǔ)義
    2.3 dL模型在形式化驗(yàn)證中的優(yōu)勢(shì)
    2.4 微分動(dòng)態(tài)邏輯的推理演算法則
    2.5 鐵路道口控制系統(tǒng)分析與建模
        2.5.1 鐵路道口控制系統(tǒng)分析
        2.5.2 鐵路道口控制系統(tǒng)建模
    2.6 本章小結(jié)
第三章 結(jié)構(gòu)分析與設(shè)計(jì)語(yǔ)言對(duì)CPS的建模
    3.1 結(jié)構(gòu)設(shè)計(jì)與分析語(yǔ)言介紹
        3.1.1 AADL概念
        3.1.2 AADL組件
    3.2 溫度無(wú)線傳感器網(wǎng)絡(luò)模型
        3.2.1 溫度無(wú)線傳感器網(wǎng)絡(luò)
        3.2.2 模型的建立
    3.3 本章小結(jié)
第四章 時(shí)鐘理論對(duì)CPS的建模
    4.1 時(shí)鐘理論的基本概念
    4.2 時(shí)鐘理論的建模
        4.2.1 溫度控制系統(tǒng)的時(shí)鐘理論建模
        4.2.2 鐵路道口控制的時(shí)鐘理論建模
    4.3 本章小結(jié)
第五章 建模與驗(yàn)證的工具
    5.1 基于微分動(dòng)態(tài)邏輯模型的工具KeYmaera
    5.2 基于KeYmaera的性質(zhì)驗(yàn)證
    5.3 AADL建模工具
    5.4 本章小結(jié)
第六章 總結(jié)與展望
    6.1 總結(jié)
    6.2 展望
附錄A
    A.1 火車(chē)道口控制系統(tǒng)安全性驗(yàn)證的KeYmaera程序
    A.2 AADL文本形式建模代碼
參考文獻(xiàn)
攻讀碩士學(xué)位期間發(fā)表論文和參與科研項(xiàng)目情況
致謝



本文編號(hào)：3930836