可程式嵌入式系統形式化建模與自動驗證技術的研究

《可程式嵌入式系統形式化建模與自動驗證技術的研究》是依託清華大學，由羅貴明擔任項目負責人的面上項目。

基本介紹

• 中文名：可程式嵌入式系統形式化建模與自動驗證技術的研究
• 依託單位：清華大學
• 項目負責人：羅貴明

項目摘要

可程式嵌入式系統能更好地滿足工程的需要，在眾多行業中得到廣泛使用。隨著計算技術的發展，嵌入式軟體的規模和複雜性不斷增加，計算系統的可靠性更顯得重要。模型檢測技術能驗證一個系統是否滿足其屬性，查找系統出現的錯誤，從而降低由於在系統部署前未發現錯誤而導致災難性後果的風險。本項目研究可程式嵌入式系統計算技術的可靠性。提取系統關鍵的屬性，採用形式化方法對嵌入式系統建模、抽象、精化和自動檢測。利用自適應技術探討嵌入式軟體黑箱模型的自適應建模理論和檢測方法。研究模型和屬性的分解，提出系統和組件一致性的驗證方法。將可滿足度方法用於模型檢測中，建立基於可滿足度的推理框架可信的網路推理系統；改進UML模型檢測工具，提出一個檢測UML模型的驗證方法。改進自動機轉換和最佳化驗證搜尋算法，減少自動機狀態數量，緩解狀態爆炸問題。套用本項目的理論和方法，建立和完善嵌入式系統的模型檢測工具，並對實際PLC系統作檢測驗證。

結題摘要

本項目研究可程式嵌入式系統計算技術的可靠性。研究了複雜系統的自適應建模算法和嵌入式軟體黑箱模型的自適應建模理論和檢測方法。利用SVM和神經網路研究了系統建模方法，提出了適合不同需求的自適應算法；改進了可滿足度求解算法，研究了時序邏輯的可滿足度；利用可滿足度理論研究了推理框架；對模型檢測及算法作了深入的研究，給出時序邏輯到自動機的直接轉換算法，將LTL 公式一次性轉換為基於遷移的Büchi 自動機。研究了嵌入式系統的環境建模和時間自動機建模，提出了環境的劃分與合併的算法、時間抽象和建模的方法。將加權自動機用於組合電路的時序建模，提出了事件傳播加權自動機模型。研究了UML狀態圖的隨機和連續時間屬性。分析了帶有時間自動機的CSL語言，將時間屬性引入檢測體系，並將其和帶有命題和機率的狀態圖結合起來，提出了針對狀態圖的隨機和時間屬性的模型檢測方法。對全稱CTL給出了有界模型檢測方法，給出了邏輯公式對無界情形的檢測特點和證據滿足的條件。提出了模組建模與模型檢測一體化檢測方法，並設計模型檢測工具，對可程式嵌入式軟體進行檢測。