《信息物理融合系統建模與驗證關鍵技術研究》是依託東南大學，由周穎擔任項目負責人的面上項目。
基本介紹
- 中文名：信息物理融合系統建模與驗證關鍵技術研究
- 項目類別：面上項目
- 項目負責人：周穎
- 依託單位：東南大學
中文摘要,結題摘要,
中文摘要
在信息化和網路化的浪潮中，物理設備的計算、通信和控制能力日益增強，將三者融為一體的信息物理融合系統（CPS）的研究和開發近年來不僅受到學術機構和企業界的廣泛關注，還受到很多國家政府的大力支持。而隨著CPS在各行各業的推廣套用，CPS本身一些關鍵屬性（如安全性、時態屬性、可靠性和可信性等）以及關鍵算法和協定是否滿足需求就顯得特別重要。本項目從考察傳統的混成系統研究過程出發，借鑑混成建模與屬性驗證的成功經驗，擬用一種擴展的UML建模語言、屬性序列圖（PSC）和微分動態邏輯（DDL）分別對CPS進行軟體規約、建模與形式驗證，通過引入PSC和擴展的DDL證明規則，力爭對CPS系統的關鍵屬性、算法和協定進行系統地描述和驗證。本項目旨在建立一套完整的針對CPS的軟體規約、建模與驗證理論和方法。研究過程中還結合智慧型交通系統等實際CPS，對其關鍵屬性、算法和協定進行深入的形式驗證、實證分析和評估。
結題摘要
（1）為解決微分時態動態邏輯（dTL）表達能力弱以及微分代數動態邏輯(DAL)缺少時序表達能力的問題，提出了一種結合dTL和DAL的微分代數動態時態邏輯（DATL）。採用微分代數程式（DAP）作為操作模型，使DAL具有dTL的時序處理能力。定義了DATL操作模型的DAP和DATL語法，給出了DAP的跡語義和DATL語義，在繼承dTL和DAL規則的基礎上新增了6個規則。通過對飛機避撞系統安全性的規約和驗證，檢驗了DATL的有效性。（2）定義了微分代數程式的跡語義，使得利用微分代數程式建立的模型對帶有時序特徵的屬性規約和驗證時發揮作用；定義了DATL公式的語法和語義，利用DATL對帶有時序特徵的CPS屬性進行規約； 在繼承微分代數動態邏輯(DAL)和微分時序動態邏輯增(dTL)規則的基礎上，增加了六條新規則，並對這些規則給予了合理性證明；驗證了三維飛機避撞系統中帶有時序特徵的安全性屬性。
