《基於實時連續環境的嵌入式系統的模型檢測技術研究》是依託西安電子科技大學，由張海賓擔任項目負責人的面上項目。
基本介紹
- 中文名：基於實時連續環境的嵌入式系統的模型檢測技術研究
- 項目類別：面上項目
- 項目負責人：張海賓
- 依託單位：西安電子科技大學
中文摘要,結題摘要,
中文摘要
本項目以模型檢測技術在確保嵌入式系統的可靠性和安全性中的套用為研究背景，探索嵌入式系統的軟硬體系統正確性以及嵌入式系統的實時性和連續性質的驗證方法。基於計算機科學，最佳化數學以及控制學等學科的相關理論，建立邏輯電路到自動機、嵌入式軟體代碼到區間時序邏輯的可執行子集的轉換規則和區間時序邏輯的模型檢測算法進行嵌入式軟硬體系統的正確性驗證；建立時間區間時序邏輯到時間自動機的轉換規則和基於BDD結構的時間自動機的高效的可達性分析算法驗證嵌入式系統的實時性質；建立線性混合系統可達性分析的約束凸多面體模型和基於約束求解、高斯消去等技術的可達集分析算法，以及非線性混合系統到線性混合系統的近似算法和抽象加細規則用於驗證嵌入式系統的連續性質。這些技術對確保嵌入式系統的可靠性和安全性將有重要作用，並可為嵌入式系統設計提供修正的反饋。
結題摘要
本項目研究嵌入式系統的軟硬體建模方法和區間時序邏輯的模型檢測算法進行嵌入式軟硬體系統的正確性驗證，研究時間區間時序邏輯模型檢測算法驗證嵌入式系統的實時性質，研究線性混合系統的可達性分析結構和非線性混合系統的近似驗證算法。 取得的研究成果包括：（1）構建了基於時序邏輯語言MSVL的系統建模、仿真方法和基於區間時序邏輯的擴展--命題投影時序邏輯的系統性質驗證方法；（2）通過轉化為離散時間區間時序邏輯可滿足性判定問題解決了實時系統的模型檢測問題，解決了同一邏輯框架內無法自動驗證實時系統的實時性質的問題；（3）構建了線性混合系統具有可判定的可達性問題的最大子集--矩形混合系統的可達性分析模型和算法；（4）構建了用於嵌入式穿戴設備的錯誤檢測和數據修復的隱馬爾科夫模型、貝葉斯模型和距離模型，以及基於這些模型的錯誤檢測和數據修復算法以確保嵌入式穿戴設備的數據可靠性；（5）構建了感測器網路的防竊聽模型和協作干擾方法以保證數據的可靠性；（6）建立了嵌入式通信設備中斷機率測試方法和多目標免疫最最佳化算法；（7）提出了一種可持續性秘籍移動群智感知的擁塞感知通信範式以實現移動群智感知中的有效負載均衡和通信的可靠性。這些技術為確保嵌入式系統的可靠性和安全性提供了重要作用，同時為嵌入式系統的設計提供了修正反饋。
