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

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

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

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

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