本文關鍵詞：基于SysML活動圖的嵌入式實時系統(tǒng)安全性驗證方法研究

  更多相關文章： 嵌入式實時系統(tǒng) 安全性 SysML活動圖 MARTE時鐘 時間自動機 模型檢測

【摘要】：嵌入式實時系統(tǒng)在航空航天、核電及交通等安全關鍵領域中廣泛使用,規(guī)模變得愈發(fā)龐大,體系結構變得更復雜,其故障引起的安全事故有著顯著的社會影響,甚至造成災難性的后果。因此,對嵌入式實時系統(tǒng)設計進行安全性分析與驗證成為學術界和工業(yè)界亟需攻克的難點。UML(United Modeling Language)常被用來軟件設計建模,但在建模能力上不能滿足嵌入式實時系統(tǒng)建模需求且缺乏非功能屬性建模元素;半形式化的模型在安全性驗證上難以被直接使用。針對以上問題,本文提出一種擴展MARTE(Modeling and Analysis of Real-time and Embedded Systems)時鐘語義信息到Sys ML(System Modeling Language)活動圖(Sys ML/MARTE活動圖)的嵌入式實時系統(tǒng)安全性驗證方法,彌補了UML在針對嵌入式實時系統(tǒng)建模及驗證上的不足。主要內容如下:首先,針對嵌入式實時系統(tǒng),提出使用Sys ML/MARTE活動圖對嵌入式實時系統(tǒng)進行建模,包括采用適合系統(tǒng)建模的Sys ML活動圖構建功能流模型及擴展MARTE時鐘語義來構建時間非功能屬性。然后,通過基于元模型的模型轉換方法將Sys ML/MARTE活動圖轉換到時間自動機,包括:(1)針對Sys ML活動圖以及MARTE時鐘等建模元素,分別構建其同構的元模型,并在元模型體系中將MARTE語義信息添加到Sys ML活動圖,構建時間自動機的元模型;(2)給出Sys ML/MARTE活動圖和時間自動機的元模型在類型、行為以及時間等元素上的語義映射規(guī)則,給出Sys ML/MARTE活動圖嵌套、分支和并發(fā)結構到時間自動機的轉換規(guī)則,將Sys ML/MARTE活動圖模型轉換為時間自動機模型;(3)通過語法轉換,將時間自動機模型轉換為模型檢測工具UPPAAL可以直接使用的時間自動機文本。最后,根據(jù)嵌入式實時系統(tǒng)設計安全需求,提取CTL(computation temporal logic)規(guī)約,在UPPAAL下對轉換得到的時間自動機進行安全性分析與驗證。
【關鍵詞】：嵌入式實時系統(tǒng) 安全性 SysML活動圖 MARTE時鐘 時間自動機 模型檢測
【學位授予單位】：南京航空航天大學
【學位級別】：碩士
【學位授予年份】：2015
【分類號】：TP368.1;TP309
【目錄】：

• 摘要4-5
• ABSTRACT5-10
• 縮略詞10-11
• 第一章 緒論11-16
• 1.1 課題研究背景及意義11-12
• 1.2 研究現(xiàn)狀及選題依據(jù)12-14
• 1.2.1 研究現(xiàn)狀12-13
• 1.2.2 選題依據(jù)13-14
• 1.3 論文組織結構14-16
• 第二章 面向嵌入式實時系統(tǒng)安全性驗證的SYSML活動圖轉換方法16-28
• 2.1 嵌入式實時系統(tǒng)安全性問題分析16-17
• 2.1.1 嵌入式實時系統(tǒng)特點16-17
• 2.1.2 安全性驗證的必要性17
• 2.2 基于MDA的模型轉換方法17-20
• 2.2.1 縱向模型轉換18-19
• 2.2.2 橫向模型轉換19-20
• 2.3 面向嵌入式實時系統(tǒng)安全性驗證的SYSML活動圖轉換20-27
• 2.3.1 Sys ML活動圖特點20-22
• 2.3.2 MARTE時鐘結構22-25
• 2.3.3 面向嵌入式實時系統(tǒng)安全性驗證的擴展Sys ML活動圖轉換框架25-27
• 2.4 本章小結27-28
• 第三章 SYSML/MARTE活動圖元建模與時間自動機元建模28-43
• 3.1 異構元模型的同構化28-31
• 3.1.1 異構元模型的根-元元模型28-30
• 3.1.2 異構元模型的同構化方法30-31
• 3.2 SYSML/MARTE活動圖元建模31-36
• 3.2.1 Sys ML活動圖的語法結構31-32
• 3.2.2 Sys ML活動圖元建模32-34
• 3.2.3 MARTE時鐘元建模34-36
• 3.3 UPPAAL時間自動機元建模36-42
• 3.3.1 UPPAAL時間自動機語法及語義36-38
• 3.3.2 數(shù)據(jù)類型元建模38-39
• 3.3.3 表達式元建模39-40
• 3.3.4 組成結構元建模40-42
• 3.4 本章小結42-43
• 第四章 SYSML/MARTE活動圖到時間自動機的轉換43-57
• 4.1 基于AMMA的活動圖到時間自動機的元模型轉換框架43-46
• 4.1.1 AMMA平臺異構模型轉換方法43-44
• 4.1.2 AMMA平臺異構模型轉換實施過程44-46
• 4.2 SYSML/MARTE活動圖與時間自動機元模型間語義映射46-49
• 4.2.1 類型結構元素的語義映射46-47
• 4.2.2 活動行為元素的語義映射47-48
• 4.2.3 時間元素的語義映射48-49
• 4.3 SYSML/MARTE活動圖與時間自動機的結構轉換49-54
• 4.3.1 嵌套結構的轉換49-51
• 4.3.2 并發(fā)結構的轉換51-53
• 4.3.3 分支結構的轉換53-54
• 4.4 時間自動機模型到時間自動機文本的語法轉換54-56
• 4.5 本章小結56-57
• 第五章 緊急呼叫系統(tǒng)設計安全性驗證57-67
• 5.1 緊急呼叫系統(tǒng)需求描述57
• 5.2 緊急呼叫系統(tǒng)SYSML/MARTE活動圖建模57-61
• 5.3 緊急呼叫系統(tǒng)SYSML/MARTE活動圖到時間自動機轉換61-64
• 5.4 緊急呼叫系統(tǒng)設計的安全性驗證與分析64-66
• 5.5 本章小結66-67
• 第六章 總結與展望67-69
• 6.1 論文工作總結67
• 6.2 進一步工作67-69
• 參考文獻69-75
• 致謝75-76
• 在學期間的研究成果及發(fā)表的學術論文76

【相似文獻】

中國期刊全文數(shù)據(jù)庫 前10條

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

2 管昌生，夏紅霞，劉定飛，，鐘珞;一種結構程序設計與分析的工具[J];微電子學與計算機;1994年05期

3 王智群;;一種Concur任務樹轉化為UML2.0的方法[J];計算機工程;2009年11期

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

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

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

7 杜薇,劉偉;UML的活動圖及其在電子政務項目中的應用[J];計算機工程;2003年05期

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

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

10 許永峰;陳平;;基于UML活動圖的進程關系模型恢復方法[J];電子科技;2006年05期

中國重要會議論文全文數(shù)據(jù)庫 前3條

1 唐劍文;;基于UML嵌套活動圖的回歸測試用例選擇[A];全國第21屆計算機技術與應用學術會議（CACIS·2010）暨全國第2屆安全關鍵技術與應用學術會議論文集[C];2010年

2 韋銀星;張申生;曹健;;基于UML活動圖的軟件過程模型研究[A];第六屆全國計算機應用聯(lián)合學術會議論文集[C];2002年

3 陳章耀;李曉峰;;基于UML活動圖的電信業(yè)務過程建模方法[A];2008'中國信息技術與應用學術論壇論文集（一）[C];2008年

中國重要報紙全文數(shù)據(jù)庫 前2條

1 記者 朱周良;美再謀劃時代突破：斥巨資繪人腦活動圖[N];上海證券報;2013年

2 本報記者 沈湫莎;繪制人腦活動圖，10年太短[N];文匯報;2013年

中國碩士學位論文全文數(shù)據(jù)庫 前10條

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

2 常旭嶺;基于Petri網(wǎng)的“系統(tǒng)的系統(tǒng)”的建模與仿真的研究[D];上海交通大學;2015年

3 惠文濤;基于概率模型檢測的SysML活動圖驗證方法研究[D];解放軍信息工程大學;2015年

4 俞磊;基于UML活動圖的仿真與測試方法研究[D];南京大學;2014年

5 李慶;基于UML活動圖的測試用例生成方法的研究[D];江蘇科技大學;2016年

6 黃傳林;基于SysML活動圖的嵌入式實時系統(tǒng)安全性驗證方法研究[D];南京航空航天大學;2015年

7 胡良文;基于SPIN的UML模型一致性驗證的研究及應用[D];南京航空航天大學;2015年

8 曹偉芳;基于SysML活動圖的測試序列生成方法研究[D];南昌航空大學;2016年

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

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

本文編號：636747