安全關(guān)鍵嵌入式系統(tǒng)的SysML活動圖概率驗證方法研究.pdf

1、嵌入式系統(tǒng)已經(jīng)在航空航天、交通運輸、核電能源等安全關(guān)鍵領(lǐng)域得到了廣泛運用，系統(tǒng)故障引起的安全事故往往會造成不可挽回的災(zāi)難性后果。保證嵌入式系統(tǒng)的可靠性與安全性已經(jīng)成為學術(shù)界和工業(yè)界共同關(guān)注的重點課題之一。SysML(Systems Modeling Language)是基于UML2.0提出的系統(tǒng)建模語言。SysML活動圖擴展了概率屬性，是最適合對系統(tǒng)的動態(tài)行為建模的方法之一。概率模型檢測是基于模型檢測技術(shù)的概率驗證方法，能夠?qū)ο到y(tǒng)模型的

2、隨機特征、時間特征及空間特征進行綜合描述與驗證。
　　本文結(jié)合SysML活動圖和概率模型檢測方法，針對系統(tǒng)的概率事件和外部環(huán)境的不確定因素，提出一種面向安全關(guān)鍵嵌入式系統(tǒng)的SysML活動圖概率驗證方法，在系統(tǒng)開發(fā)的早期以較小代價發(fā)現(xiàn)并修正嵌入式系統(tǒng)中存在的缺陷。論文主要研究內(nèi)容包括：
　?。?）提出基于馬爾可夫決策過程(Markov Decision Process, MDP)的SysML活動圖概率模型構(gòu)建方法。首先，給出嵌

3、套活動圖的分解算法。然后，定義描述活動圖狀態(tài)遷移的MDP表達式，并基于MDP表達式描述活動圖的概率模型。最后，給出活動圖到MDP表達式的轉(zhuǎn)換算法，實現(xiàn)SysML活動圖概率模型的自動構(gòu)建。
　?。?）提出利用概率模型檢測工具PRISM驗證并分析SysML活動圖概率模型的方法。首先，給出MDP表達式到PRISM代碼的轉(zhuǎn)換規(guī)則，實現(xiàn)活動圖概率模型到PRISM模型的轉(zhuǎn)換。然后，利用概率計算樹邏輯(Probabilistic computa

4、tion tree logic, PCTL)描述待驗證的安全性質(zhì)規(guī)約。最后，將活動圖概率模型與PCTL表達式導入PRISM驗證并分析結(jié)果。
　?。?）設(shè)計實現(xiàn)模型轉(zhuǎn)換工具SAD2PRISM，并結(jié)合本文方法使用SAD2PRISM分析飛機起落架系統(tǒng)的實例。首先，給出模型轉(zhuǎn)換工具SAD2PRISM的設(shè)計思想與實現(xiàn)方式。然后，利用SAD2PRISM對飛機起落架系統(tǒng)著陸流程的活動圖概率建模。最后，利用PRISM驗證起落架系統(tǒng)是否滿足性質(zhì)規(guī)約