信息物理融合系統(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ù),是國內(nèi)外信息技術(shù)領(lǐng)域研究的一類重要系統(tǒng)。如何對(duì)CPS系統(tǒng)進(jìn)行建模,以及驗(yàn)證模型中的性質(zhì)以確保CPS系統(tǒng)的保真性、可靠性等特點(diǎn)是一個(gè)重要的研究問題。 本文主要采用微分動(dòng)態(tài)邏輯(Differential Dynamic Logic, dL)、結(jié)構(gòu)分析與設(shè)計(jì)語言(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)行形式化建模與分析。從火車發(fā)送接近信號(hào)到進(jìn)入道口的運(yùn)動(dòng)過程中,針對(duì)火車到達(dá)道口的時(shí)間要求,將火車速度控制問題抽象成一個(gè)混成系統(tǒng)的安全性性質(zhì),用微分動(dòng)態(tài)邏輯來描述,并使用混成系統(tǒng)證明工具KeYmaera對(duì)系統(tǒng)的安全性進(jìn)行了驗(yàn)證,實(shí)現(xiàn)對(duì)火車進(jìn)入...

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

【學(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 國內(nèi)外研究現(xiàn)狀
    1.3 研究內(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 混成程序的語法語義
    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ì)語言對(duì)CPS的建模
    3.1 結(jié)構(gòu)設(shè)計(jì)與分析語言介紹
        3.1.1 AADL概念
        3.1.2 AADL組件
    3.2 溫度無線傳感器網(wǎng)絡(luò)模型
        3.2.1 溫度無線傳感器網(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 火車道口控制系統(tǒng)安全性驗(yàn)證的KeYmaera程序
    A.2 AADL文本形式建模代碼
參考文獻(xiàn)
攻讀碩士學(xué)位期間發(fā)表論文和參與科研項(xiàng)目情況
致謝



本文編號(hào)：3930836