發(fā)布時間：2021-02-18 00:37

　　近些年來,隨著系統(tǒng)設(shè)計(jì)復(fù)雜性的提高,各種系統(tǒng)錯誤在實(shí)際應(yīng)用中層出不窮,其造成嚴(yán)重后果的事件也逐年增多。系統(tǒng)建模是如今眾多系統(tǒng)設(shè)計(jì)所必不可少的一個環(huán)節(jié),同時作為整個系統(tǒng)設(shè)計(jì)流程的開始,提高其模型的正確性對減少后期生成系統(tǒng)的各類錯誤至關(guān)重要。針對系統(tǒng)設(shè)計(jì)過程中生成的多種模型進(jìn)行正確性分析與驗(yàn)證,可以盡早發(fā)現(xiàn)設(shè)計(jì)漏洞,改正設(shè)計(jì)錯誤,減少系統(tǒng)問題的出現(xiàn)。所謂模型設(shè)計(jì)的正確性就是指所設(shè)計(jì)出的模型是否能正確表達(dá)未來真實(shí)系統(tǒng)的某種功能或者某些特性,如果能客觀的反應(yīng)出真實(shí)系統(tǒng)的一些指標(biāo)特性,那么這樣的模型就是正確的。被設(shè)計(jì)出的模型的正確與否,與后期生成真實(shí)系統(tǒng)的可用性和可靠性密切相關(guān)。系統(tǒng)建模語言（Systems Modeling Language,SysML）作為軟件工程和系統(tǒng)工程領(lǐng)域的標(biāo)準(zhǔn)建模語言,近些年被設(shè)計(jì)人員開始大量使用。SysML針對系統(tǒng)工程領(lǐng)域中系統(tǒng)設(shè)計(jì)與建模的特點(diǎn),提供了可視化、圖形化的系統(tǒng)建模支持,其中Sys ML活動圖的應(yīng)用尤為廣泛。但由于其為了保持建模的易于理解和高效簡單,在進(jìn)行語義說明時SysML采用了和UML相似的半形式化描述方法,使用自然語言對相應(yīng)語義進(jìn)行描述,這就造成了其... 

【文章來源】：戰(zhàn)略支援部隊(duì)信息工程大學(xué)河南省

【文章頁數(shù)】：73 頁

【學(xué)位級別】：碩士

【文章目錄】：
摘要
Abstract
第一章 緒論
    1.1 研究背景和意義
    1.2 國內(nèi)外研究現(xiàn)狀
    1.3 本文研究內(nèi)容
    1.4 論文組織結(jié)構(gòu)
第二章 相關(guān)知識介紹
    2.1 SysML概述
        2.1.1 SysML的產(chǎn)生和發(fā)展
        2.1.2 SysML的圖形表示
    2.2 模型檢測技術(shù)
        2.2.1 模型檢測定義
        2.2.2 模型檢測特點(diǎn)
    2.3 概率模型檢測技術(shù)
        2.3.1 離散馬爾科夫鏈模型
        2.3.2 連續(xù)馬爾科夫鏈模型
        2.3.3 概率自動機(jī)模型
        2.3.4 三種模型的比較分析
    2.4 本章小結(jié)
第三章 基于新活動演算的SysML活動圖形式化描述
    3.1 SysML活動圖
    3.2 SysML活動圖在新活動演算中語法表示
    3.3 SysML活動圖的語義表示
        3.3.1 動作節(jié)點(diǎn)
        3.3.2 行為調(diào)用
        3.3.3 并發(fā)節(jié)點(diǎn)
        3.3.4 決策節(jié)點(diǎn)
        3.3.5 合并節(jié)點(diǎn)
        3.3.6 同步節(jié)點(diǎn)
        3.3.7 發(fā)送和接收
        3.3.8 流程結(jié)束和活動結(jié)束
    3.4 應(yīng)用實(shí)例
    3.5 本章小結(jié)
第四章 基于概率模型檢測器的SysML活動圖形式化驗(yàn)證
    4.1 PRISM定義
        4.1.1 PRISM程序定義
        4.1.2 PRISM語法定義
        4.1.3 PRISM語義定義
    4.2 SysML活動圖到PRISM輸入的轉(zhuǎn)換
        4.2.1 SysML活動圖相應(yīng)術(shù)語在PRISM中的表示
        4.2.2 SysML活動圖到PRISM代碼的轉(zhuǎn)化算法
        4.2.3 PCTL性質(zhì)規(guī)格說明
    4.3 驗(yàn)證方法
    4.5 本章小結(jié)
第五章 交互式電子技術(shù)手冊的SysML活動圖建模與驗(yàn)證
    5.1 系統(tǒng)介紹
    5.2 實(shí)驗(yàn)平臺簡介
    5.3 系統(tǒng)SysML活動圖建模
    5.4 系統(tǒng)SysML活動圖驗(yàn)證
    5.5 本章小結(jié)
第六章 總結(jié)與展望
    6.1 本文工作總結(jié)
    6.2 下一步工作
致謝
參考文獻(xiàn)
作者簡歷


【參考文獻(xiàn)】：
期刊論文
[1]基于Spin的SysML活動圖驗(yàn)證框架[J]. 胡良文,馬金晶,孫博.  計(jì)算機(jī)科學(xué)與探索. 2014(07)
[2]Towards a Formal Semantics for UML/MARTE State Machines Based on Hierarchical Timed Automata[J]. 周宇,Luciano Baresi,Matteo Rossi.  Journal of Computer Science & Technology. 2013(01)
[3]基于UML的地空導(dǎo)彈武器系統(tǒng)IETM建模[J]. 王學(xué)智,邵孟國,胡鄧華.  計(jì)算機(jī)測量與控制. 2011(11)
[4]基于CPN的UML2.0形式化建模[J]. 孔瑩瑩,蒲海濤,隋瑞升.  青島大學(xué)學(xué)報(工程技術(shù)版). 2011(01)
[5]IETM技術(shù)發(fā)展綜述及其特點(diǎn)分析[J]. 陸洪武,陳建國,王榮穎.  艦船電子工程. 2009(07)
[6]裝備交互式電子技術(shù)手冊發(fā)展綜述[J]. 梁偉杰,于永利,張磊,杜曉明.  國防技術(shù)基礎(chǔ). 2009(05)
[7]SysML:一種新的系統(tǒng)建模語言[J]. 蔣彩云,王維平,李群.  系統(tǒng)仿真學(xué)報. 2006(06)
[8]UML活動圖的時序邏輯語義[J]. 朱雪陽,唐稚松.  計(jì)算機(jī)研究與發(fā)展. 2005(09)
[9]UML順序圖的自動驗(yàn)證[J]. 王璐珍,董威,陳火旺.  計(jì)算機(jī)工程與應(yīng)用. 2003(29)
[10]基于Z規(guī)范的統(tǒng)一建模語言序列圖語義分析方法[J]. 李景峰,陳平.  西安電子科技大學(xué)學(xué)報. 2003(04)

碩士論文
[1]SysML行為圖到Petri網(wǎng)的轉(zhuǎn)換研究[D]. 王松鋒.解放軍信息工程大學(xué) 2012



本文編號：3038784