嵌入式系統(tǒng)已經(jīng)在航空航天、交通運(yùn)輸、核電能源等安全關(guān)鍵領(lǐng)域得到了廣泛運(yùn)用,系統(tǒng)故障引起的安全事故往往會造成不可挽回的災(zāi)難性后果。保證嵌入式系統(tǒng)的可靠性與安全性已經(jīng)成為學(xué)術(shù)界和工業(yè)界共同關(guān)注的重點(diǎn)課題之一。SysML(Systems Modeling Language)是基于UML2.0提出的系統(tǒng)建模語言。SysML活動圖擴(kuò)展了概率屬性,是最適合對系統(tǒng)的動態(tài)行為建模的方法之一。概率模型檢測是基于模型檢測技術(shù)的概率驗(yàn)證方法,能夠?qū)ο到y(tǒng)模型的隨機(jī)特征、時間特征及空間特征進(jìn)行綜合描述與驗(yàn)證。本文結(jié)合SysML活動圖和概率模型檢測方法,針對系統(tǒng)的概率事件和外部環(huán)境的不確定因素,提出一種面向安全關(guān)鍵嵌入式系統(tǒng)的SysML活動圖概率驗(yàn)證方法,在系統(tǒng)開發(fā)的早期以較小代價發(fā)現(xiàn)并修正嵌入式系統(tǒng)中存在的缺陷。論文主要研究內(nèi)容包括:(1)提出基于馬爾可夫決策過程(Markov Decision Process,MDP)的SysML活動圖概率模型構(gòu)建方法。首先,給出嵌套活動圖的分解算法。然后,定義描述活動圖狀態(tài)遷移的MDP表達(dá)式,并基于MDP表達(dá)式描述活動圖的概率模型。最后,給出活動圖到MDP表達(dá)式的轉(zhuǎn)換算法,實(shí)現(xiàn)SysML活動圖概率模型的自動構(gòu)建。(2)提出利用概率模型檢測工具PRISM驗(yàn)證并分析SysML活動圖概率模型的方法。首先,給出MDP表達(dá)式到PRISM代碼的轉(zhuǎn)換規(guī)則,實(shí)現(xiàn)活動圖概率模型到PRISM模型的轉(zhuǎn)換。然后,利用概率計算樹邏輯(Probabilistic computation tree logic,PCTL)描述待驗(yàn)證的安全性質(zhì)規(guī)約。最后,將活動圖概率模型與PCTL表達(dá)式導(dǎo)入PRISM驗(yàn)證并分析結(jié)果。(3)設(shè)計實(shí)現(xiàn)模型轉(zhuǎn)換工具SAD2PRISM,并結(jié)合本文方法使用SAD2PRISM分析飛機(jī)起落架系統(tǒng)的實(shí)例。首先,給出模型轉(zhuǎn)換工具SAD2PRISM的設(shè)計思想與實(shí)現(xiàn)方式。然后,利用SAD2PRISM對飛機(jī)起落架系統(tǒng)著陸流程的活動圖概率建模。最后,利用PRISM驗(yàn)證起落架系統(tǒng)是否滿足性質(zhì)規(guī)約,發(fā)現(xiàn)問題并予以改進(jìn),保證系統(tǒng)的可靠性與安全性。
【學(xué)位單位】：南京航空航天大學(xué)
【學(xué)位級別】：碩士
【學(xué)位年份】：2015
【中圖分類】：TP368.1
【文章目錄】：
摘要
abstract
縮略詞
第一章 緒論
    1.1 課題研究背景
    1.2 國內(nèi)外研究現(xiàn)狀及選題依據(jù)
        1.2.1 SYSML建模相關(guān)研究現(xiàn)狀
        1.2.2 概率模型檢測相關(guān)研究現(xiàn)狀
        1.2.3 選題依據(jù)
    1.3 論文組織結(jié)構(gòu)
第二章 面向嵌入式系統(tǒng)的SYSML活動圖概率驗(yàn)證方法概述
    2.1 SYSML活動圖
        2.1.1 SYSML活動圖基本元素
        2.1.2 SYSML活動圖的特點(diǎn)
    2.2 形式化建模與驗(yàn)證方法
        2.2.1 形式化方法概述
        2.2.2 概率模型檢測方法的特點(diǎn)
    2.3 面向嵌入式系統(tǒng)的SYSML活動圖概率驗(yàn)證總體框架
    2.4 本章小結(jié)
第三章 基于馬爾可夫決策過程的SYSML活動圖概率模型構(gòu)建
    3.1 嵌套活動圖的分解
    3.2 基于馬爾可夫決策過程的活動圖概率建模
        3.2.1 馬爾可夫決策過程MDP
        3.2.2 活動圖概率模型的定義和約束
        3.2.3 基于MDP表達(dá)式的活動圖概率模型描述
    3.3 活動圖概率模型的自動構(gòu)建
    3.4 本章小結(jié)
第四章 SYSML活動圖概率模型的安全性分析與驗(yàn)證
    4.1 SYSML活動圖概率模型到PRISM模型的轉(zhuǎn)換
        4.1.1 概率模型檢測工具PRISM
        4.1.2 MDP表達(dá)式到PRISM代碼的轉(zhuǎn)換規(guī)則
    4.2 SYSML活動圖概率模型的PRISM驗(yàn)證
        4.2.1 基于概率計算樹邏輯表示的需求規(guī)約
        4.2.2 活動圖模型的PRISM概率模型檢測
    4.3 本章小結(jié)
第五章 飛機(jī)起落架系統(tǒng)的安全性分析與驗(yàn)證
    5.1 活動圖模型轉(zhuǎn)換工具SAD2PRISM的設(shè)計與實(shí)現(xiàn)
    5.2 飛機(jī)起落架系統(tǒng)活動圖概率模型的構(gòu)建
    5.3 飛機(jī)起落架系統(tǒng)概率模型的安全性分析與驗(yàn)證
    5.4 本章小結(jié)
第六章 總結(jié)與展望
    6.1 論文工作總結(jié)
    6.2 未來工作展望
參考文獻(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);余祥;;基于形式活動圖的協(xié)議一致性測試用例生成方法研究[J];安徽大學(xué)學(xué)報(自然科學(xué)版);2013年03期

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

本文編號：2848083