《信息物理融合系統軟體可信性驗證方法研究》是依託大連理工大學,由侯剛擔任項目負責人的青年科學基金項目。
基本介紹
- 中文名：信息物理融合系統軟體可信性驗證方法研究
- 依託單位：大連理工大學
- 項目類別：青年科學基金項目
- 項目負責人：侯剛
項目摘要,結題摘要,
項目摘要
信息物理融合系統（Cyber Physical Systems，CPS）作為當今世界信息技術制高點，將廣泛套用於電力系統、醫療儀器設備、航空航天等安全攸關領域。由於CPS是一種綜合了計算進程與物理環境的新型網路化嵌入式系統，故包含種類和數目眾多的嵌入式軟體，且各軟體通過網路互動，因此如何保障這些異構軟體及其互動過程可信性已成為CPS研究熱點之一。針對這一問題，本研究擬通過多種形式化建模手段融合以及機率模型檢測技術，探索CPS軟體可信設計與驗證方法，具體包含以下兩方面內容：1、研究基於擴展的確定與隨機時間Petri網和層次化狀態遷移矩陣相融合的CPS軟體功能與時空性能一體化建模方法；2、研究基於機率模型檢測的CPS軟體功能與性能一體化驗證方法，並針對該方法研究多種驗證最佳化策略，力求緩解模型檢測過程中的狀態空間爆炸。課題的成功實施，將為高可信CPS軟體開發打下更為堅實的理論基礎。
結題摘要
信息物理系統（Cyber Physical Systems，簡稱CPS）作為當今世界信息技術制高點，已廣泛套用於各類安全攸關領域。如何保障CPS軟體可信性已成為CPS研究熱點之一。本項目在軟體設計階段，研究適用於CPS軟體的形式化建模方法、驗證方法以及分析技術，具體解決以下四方面可信性保障問題： 針對CPS軟體功能與實時性驗證問題，提出基於時間狀態遷移矩陣(Time State Transition Matrix, 簡稱TSTM)的軟體形式化建模方法。TSTM在保持STM形式語義基礎上，引入時鐘函式與時間約束，使其適用於實時CPS軟體行為刻畫。在此基礎上，提出了基於時間計算樹邏輯的TSTM模型檢測方法，為有效緩解狀態空間爆炸，模型檢測方法採用限界模型檢測(Bounded Model Checking, 簡稱BMC)技術。實驗表明本研究所提方法具有較好的求解效率，實現了在軟體設計層面邏輯功能與時間性能的一體化建模與驗證。 針對CPS軟體能耗預測與分析問題，提出了基於能耗時間狀態遷移矩陣(Energy Consumption Time State Transition Matrix, 簡稱ETSTM)的綠色軟體形式化建模方法。ETSTM在TSTM基礎上，引入基於軟體結構特徵量的能耗預測函式，並給出了基於BP神經網路的能耗預測函式擬合方法。在此基礎上，提出了基於顯示路徑搜尋和限界模型檢測的CPS軟體能耗多尺度分析算法，實現了在軟體設計層面對CPS軟體能耗的預評價。 針對CPS軟體動態性能評價問題，提出了基於擴展的確定與隨機Petri網(Extended Deterministic and Stochastic Petri Nets, 簡稱EDSPN)的CPS軟體行為模型。通過為DSPN增加非確定時間語義，使其能夠有效表示由中斷嵌套帶來的執行時間不確定問題，進而實現對中斷驅動下的CPS軟體行為有效建模。此外，針對EDSPN模型分析，提出了一種基於馬爾科夫再生理論的模型求解方法，實現對CPS軟體性能的預分析。 針對CPS軟體非確定行為定量分析問題，提出了基於連續隨機邏輯的EDSPN機率模型檢測方法，該方法採用BMC策略。實驗表明，本研究所提方法在驗證局部空間可驗證的軟體屬性時，具有較好求解效率；在驗證全局空間可驗證軟體屬性時，通過增加驗證步長可逐漸逼近驗證結果。
