《基於形式化技術的複雜機電系統可靠性評價方法研究》是依託西安交通大學，由楊培林擔任項目負責人的面上項目。
基本介紹
- 中文名：基於形式化技術的複雜機電系統可靠性評價方法研究
- 項目類別：面上項目
- 項目負責人：楊培林
- 依託單位：西安交通大學
中文摘要,結題摘要,
中文摘要
可靠性評價是複雜機電系統設計過程中的一個重要環節，也是保證複雜機電系統固有可靠性、降低潛在故障危害的一種重要手段。為解決目前複雜機電系統可靠性評價方法由於非形式化而導致的一系列問題，本項目將形式化技術引入複雜機電系統的可靠性評價。基於複雜機電系統的過程模型和功能載體的狀態變遷模型研究系統的狀態解析，利用行為樹研究系統行為過程的形式化建模，基於系統狀態並利用時態邏輯研究系統可靠性要求的形式化表達。在此基礎上，結合形式化驗證技術建立基於形式化技術的複雜機電系統可靠性評價理論與方法，開發基於形式化技術的可靠性評價系統原型，並結合實例進行驗證。項目研究旨在實現複雜機電系統可靠性評價的形式化和自動化，為準確、高效地分析評價複雜機電系統可靠性提供一條新的思路和方法。本項目研究對豐富和發展複雜機電系統的可靠性評價方法、促進我國高可靠性和安全性複雜機電系統的自主研發具有十分重要的理論意義和實用價值。
結題摘要
可靠性是衡量複雜機電系統性能的重要指標之一，但傳統的可靠性分析方法是非形式化的，分析繁瑣且容易出錯。本課題將模型檢測技術（形式化技術）引入複雜機電系統的可靠性評價，提出了基於形式化技術的複雜機電系統可靠性評價方法。基於IDEF0和IDEF3的建模思想，對IDEF0基本組件中的輸入、輸出、控制和機制進行了定義，建立了機電系統行為過程的形式化表達及行為過程中的狀態變遷網路，研究了機電系統行為過程中功能載體的狀態，對機電系統行為之間的時序表達進行了定義並據此構建了機電系統行為過程的行為流網路，從而獲得機電系統行為過程中的狀變遷序列。對複雜機電系統功能執行過程中的狀態變遷機制進行了研究，並基於機電系統的狀態變遷機制及機率行為樹的語義和句法，對機電系統功能載體狀態變遷過程中的狀態、事件、控制邏輯等表達問題進行了研究，提出了基於機率行為樹的機電系統形式化建模方法。分別針對SAL和PRISM兩種模型檢測工具，以機電系統功能載體的狀態來表征機電系統的行為特徵，對基於計算樹邏輯CTL和連續隨機邏輯CSL的可靠性要求形式化表達進行了研究，實現了複雜機電系統可靠性要求的形式化規約。在以上研究的基礎上，通過對機電系統的形式化建模及潛在故障的形式化規約，實現了基於SAL的機電系統FMEA和基於PRISM的機電系統機率FMEA（PFMEA）。研究了基於機率模型檢測的機電系統可靠性評價方法，並針對機電系統中的失效相關問題，利用機率模型檢測技術實現了對機電系統的動態可靠性評價。基於機電系統機率行為樹模型與PRISM建模語言的語義和句法，給出了由機率行為樹模型向模型檢測工具PRISM模型轉換的規則，開發了機率行為樹建模原型軟體BTEditor，基於BTEditor和機率模型檢測工具PRISM實現了基於形式化技術的複雜機電系統可靠性評價，並以數控工具機進給系統為例進了驗證。本課題研究對高效準確地評價複雜機電系統的可靠性特別是FMEA分析提供了一種有效的方法，對促進和提高複雜機電系統的可靠性和安全性具有重要的理論意義和實用價值。
