嵌入式系統(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)模型的隨機(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)開(kāi)發(fā)的早期以較小代價(jià)發(fā)現(xiàn)并修正嵌入式系統(tǒng)中存在的缺陷。論文主要研究?jī)?nèi)容包括:(1)提出基于馬爾可夫決策過(guò)程(Markov Decision Process,MDP)的SysML活動(dòng)圖概率模型構(gòu)建方法。首先,給出嵌套活動(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)建。(2)提出利用概率模型檢測(cè)工具PRISM驗(yàn)證并分析SysML活動(dòng)圖概率模型的方法。首先,給出MDP表達(dá)式到PRISM代碼的轉(zhuǎn)換規(guī)則,實(shí)現(xiàn)活動(dòng)圖概率模型到PRISM模型的轉(zhuǎn)換。然后,利用概率計(jì)算樹(shù)邏輯(Probabilistic computation 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)是否滿(mǎn)足性質(zhì)規(guī)約,發(fā)現(xiàn)問(wèn)題并予以改進(jìn),保證系統(tǒng)的可靠性與安全性。
【學(xué)位單位】：南京航空航天大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位年份】：2015
【中圖分類(lèi)】：TP368.1
【文章目錄】：
摘要
abstract
縮略詞
第一章 緒論
    1.1 課題研究背景
    1.2 國(guó)內(nèi)外研究現(xiàn)狀及選題依據(jù)
        1.2.1 SYSML建模相關(guān)研究現(xiàn)狀
        1.2.2 概率模型檢測(cè)相關(guān)研究現(xiàn)狀
        1.2.3 選題依據(jù)
    1.3 論文組織結(jié)構(gòu)
第二章 面向嵌入式系統(tǒng)的SYSML活動(dòng)圖概率驗(yàn)證方法概述
    2.1 SYSML活動(dòng)圖
        2.1.1 SYSML活動(dòng)圖基本元素
        2.1.2 SYSML活動(dòng)圖的特點(diǎn)
    2.2 形式化建模與驗(yàn)證方法
        2.2.1 形式化方法概述
        2.2.2 概率模型檢測(cè)方法的特點(diǎn)
    2.3 面向嵌入式系統(tǒng)的SYSML活動(dòng)圖概率驗(yàn)證總體框架
    2.4 本章小結(jié)
第三章 基于馬爾可夫決策過(guò)程的SYSML活動(dòng)圖概率模型構(gòu)建
    3.1 嵌套活動(dòng)圖的分解
    3.2 基于馬爾可夫決策過(guò)程的活動(dòng)圖概率建模
        3.2.1 馬爾可夫決策過(guò)程MDP
        3.2.2 活動(dòng)圖概率模型的定義和約束
        3.2.3 基于MDP表達(dá)式的活動(dòng)圖概率模型描述
    3.3 活動(dòng)圖概率模型的自動(dòng)構(gòu)建
    3.4 本章小結(jié)
第四章 SYSML活動(dòng)圖概率模型的安全性分析與驗(yàn)證
    4.1 SYSML活動(dòng)圖概率模型到PRISM模型的轉(zhuǎn)換
        4.1.1 概率模型檢測(cè)工具PRISM
        4.1.2 MDP表達(dá)式到PRISM代碼的轉(zhuǎn)換規(guī)則
    4.2 SYSML活動(dòng)圖概率模型的PRISM驗(yàn)證
        4.2.1 基于概率計(jì)算樹(shù)邏輯表示的需求規(guī)約
        4.2.2 活動(dòng)圖模型的PRISM概率模型檢測(cè)
    4.3 本章小結(jié)
第五章 飛機(jī)起落架系統(tǒng)的安全性分析與驗(yàn)證
    5.1 活動(dòng)圖模型轉(zhuǎn)換工具SAD2PRISM的設(shè)計(jì)與實(shí)現(xiàn)
    5.2 飛機(jī)起落架系統(tǒng)活動(dòng)圖概率模型的構(gòu)建
    5.3 飛機(jī)起落架系統(tǒng)概率模型的安全性分析與驗(yàn)證
    5.4 本章小結(jié)
第六章 總結(jié)與展望
    6.1 論文工作總結(jié)
    6.2 未來(lái)工作展望
參考文獻(xiàn)
致謝
在學(xué)期間的研究成果及發(fā)表的學(xué)術(shù)論文
附錄 描述飛機(jī)起落架系統(tǒng)模型的PRISM代碼
    附錄A. 初始飛機(jī)起落架系統(tǒng)模型的PRSIM代碼
    附錄B. 排除死鎖后飛機(jī)起落架系統(tǒng)模型的PRSIM代碼

【相似文獻(xiàn)】

相關(guān)期刊論文 前10條

1 齊建業(yè);李強(qiáng);余祥;;基于形式活動(dòng)圖的協(xié)議一致性測(cè)試用例生成方法研究[J];安徽大學(xué)學(xué)報(bào)(自然科學(xué)版);2013年03期

2 管昌生，夏紅霞，劉定飛，鐘珞;一種結(jié)構(gòu)程序設(shè)計(jì)與分析的工具[J];微電子學(xué)與計(jì)算機(jī);1994年05期

3 王智群;;一種Concur任務(wù)樹(shù)轉(zhuǎn)化為UML2.0的方法[J];計(jì)算機(jī)工程;2009年11期

4 張正,劉建華,吳潔明,袁山龍;利用UML活動(dòng)圖進(jìn)行業(yè)務(wù)分析[J];北方工業(yè)大學(xué)學(xué)報(bào);2003年03期

5 周新寬;陳平;李青山;;一種UML活動(dòng)圖的逆向恢復(fù)方法[J];計(jì)算機(jī)工程與應(yīng)用;2006年17期

6 孫自安,周伯生;UML活動(dòng)圖的評(píng)價(jià)和擴(kuò)展[J];計(jì)算機(jī)工程與應(yīng)用;2001年12期

7 杜薇,劉偉;UML的活動(dòng)圖及其在電子政務(wù)項(xiàng)目中的應(yīng)用[J];計(jì)算機(jī)工程;2003年05期

8 崔萌 ,李宣東 ,鄭國(guó)梁;UML實(shí)時(shí)活動(dòng)圖的形式化分析[J];計(jì)算機(jī)學(xué)報(bào);2004年03期

9 朱雪陽(yáng),唐稚松;UML活動(dòng)圖的時(shí)序邏輯語(yǔ)義[J];計(jì)算機(jī)研究與發(fā)展;2005年09期

10 許永峰;陳平;;基于UML活動(dòng)圖的進(jìn)程關(guān)系模型恢復(fù)方法[J];電子科技;2006年05期

相關(guān)碩士學(xué)位論文 前10條

1 朱羿全;安全關(guān)鍵嵌入式系統(tǒng)的SysML活動(dòng)圖概率驗(yàn)證方法研究[D];南京航空航天大學(xué);2015年

2 王志超;面向活動(dòng)圖的代碼自動(dòng)生成技術(shù)研究[D];哈爾濱工業(yè)大學(xué);2010年

3 丁娜;帶OCL約束的活動(dòng)圖多態(tài)測(cè)試方法的研究[D];重慶大學(xué);2012年

4 葉楠;基于活動(dòng)圖的軟件回歸測(cè)試用例自動(dòng)生成技術(shù)研究[D];南京大學(xué);2012年

5 何曉云;基于活動(dòng)圖驅(qū)動(dòng)的軟件需求分析方法及應(yīng)用[D];電子科技大學(xué);2008年

6 崔霞;基于UML活動(dòng)圖的測(cè)試場(chǎng)景智能化生成方法研究[D];上海師范大學(xué);2009年

7 方曉春;基于流程挖掘的角色—活動(dòng)圖建模[D];復(fù)旦大學(xué);2008年

8 邢冠男;UML活動(dòng)圖到PNML轉(zhuǎn)換的研究與實(shí)現(xiàn)[D];內(nèi)蒙古大學(xué);2009年

9 蘇翠翠;一種基于UML活動(dòng)圖生成測(cè)試用例的方法[D];南京郵電大學(xué);2011年

10 況振宇;基于UCM的場(chǎng)景可視化建模研究[D];青島大學(xué);2014年

本文編號(hào)：2848083