隨著科學技術的不斷發(fā)展,人們的生活已經慢慢步入智能信息控制化時代,背后所依賴的是各種大型高可信系統。這類系統不斷地向縱深發(fā)展,系統的控制邏輯與功能實現日趨復雜,為了進一步提高系統的性能并降低維護成本,人們對系統的可靠性和安全性提出了更高的要求。因此,優(yōu)化系統的體系架構與開發(fā)新的可信計算體系軟件便迫在眉睫,在對系統的安全性及可靠性的性能評估便顯得十分必要。而概率模型檢測技術作為傳統模型檢測的基礎上演化的一個分支,不僅能夠完成自動化的驗證,而且還能產生定量的結果,對系統的驗證提供更為詳盡的依據,對提升系統性能提供一個更加明確的方向。本文主要對高可信系統的兩個實際應用場景進行研究,結合概率模型檢測技術對系統進行建模驗證分析。本文主要所做貢獻包含如下幾個方面:(1)對于傳統嵌入式控制系統的構建故障模型的形式化程度不高的特點,本文結合概率模型檢測技術對該系統發(fā)生故障的場景進行抽象化建模,將整個過程擴展成符合嵌入式控制系統實際場景的連續(xù)時間馬爾科夫鏈的概率模型(Embedded Systems Continuous-Time Markov Chain,EMCTMC),對運行過程的三個階段提出基于概率...

【文章頁數】：67 頁

【學位級別】：碩士

【部分圖文】：

圖3.2一天內不同故障首次發(fā)生的概率趨勢圖

第三章嵌入式控制系統的概率模型檢測分析29順序，為了考慮這種情況，分別單獨驗證各種不同故障最早發(fā)生的概率。使用CSL屬性描述如下：P=?[!"down"U<=T"fail"]表示在T時間內首次發(fā)生某種故障的概率。主要討論兩種情況，分別驗證在一天和一個月內兩個時間段內不同故障首次發(fā)....

圖3.3一個月內不同故障首次發(fā)生的概率趨勢圖

第三章嵌入式控制系統的概率模型檢測分析29順序，為了考慮這種情況，分別單獨驗證各種不同故障最早發(fā)生的概率。使用CSL屬性描述如下：P=?[!"down"U<=T"fail"]表示在T時間內首次發(fā)生某種故障的概率。主要討論兩種情況，分別驗證在一天和一個月內兩個時間段內不同故障首次發(fā)....

圖3.4每種故障導致系統最終宕機概率趨勢圖

第三章嵌入式控制系統的概率模型檢測分析30以上都是驗證在一個時間段范圍內的故障發(fā)生的概率，若將時間界限去除，驗證在長期時間下故障發(fā)生的概率。CSL屬性描述如下：P=?[!"down"U"fail"]其中fail依次表示四種不同的故障情況，通過驗證得到一個穩(wěn)態(tài)的概率值，結果如表3.....

圖3.5一天內不同周期數系統宕機的概率趨勢圖

第三章嵌入式控制系統的概率模型檢測分析31終宕機的概率是隨MaxCount的增大而降低。在某種程度上，增大計時器所允許的最大周期數能提高系統的容錯性。但是綜合考慮，傳感器與輸入輸出處理器都是導致系統宕機的重要因素，需要選取合理的MaxCount值，使得系統宕機的可能性最校同時驗證....

本文編號：4007170