本文關鍵詞：基于四變量模型的系統(tǒng)安全性建模與分析方法

  更多相關文章： 嵌入式系統(tǒng)設計 系統(tǒng)安全性分析 四變量模型 AltaRica SCR方法 故障樹

【摘要】：近年來,隨著嵌入式系統(tǒng)復雜度迅速增加以及系統(tǒng)軟件規(guī)模的逐漸增大,確保嵌入式系統(tǒng)及軟件的安全可靠性成為安全關鍵系統(tǒng)工程領域(如核電站、航空航天、交通等)中的一個重要挑戰(zhàn)。由此,對系統(tǒng)進行安全性分析及驗證在安全關鍵系統(tǒng)工程領域中也顯得極為重要;與此同時,基于模型的系統(tǒng)安全性分析與驗證方法成為嵌入式安全關鍵系統(tǒng)工程領域中的一個主流方法。在基于模型的系統(tǒng)安全性分析驗證的過程中,如何對系統(tǒng)進行有效的需求分析并根據(jù)需求結果進行模型設計成為當前對嵌入式安全關鍵系統(tǒng)進行分析研究的一個重要問題。本文的主要工作是分別在系統(tǒng)需求層面以及設計層面上對基于模型的系統(tǒng)安全性分析進行研究,提出了一種基于四變量模型的系統(tǒng)安全性建模與分析方法,在利用四變量模型對系統(tǒng)進行需求分析的基礎上,采用AltaRica建模語言進行模型設計,并對如何從四變量需求模型到AltaRica設計模型進行轉換這一問題展開了研究,具體工作如下所示:(1)針對系統(tǒng)需求分析層次以及系統(tǒng)設計層次的安全性建模問題,對四變量模型與AltaRica建模語言進行了分析研究。在系統(tǒng)需求分析層,我們分析了四變量模型中所包含的四類變量以及四類關系的結構,并結合SCR需求分析方法研究了四變量模型方法的形式化語義。在系統(tǒng)設計層,我們對AltaRica建模語言也進行了分析,包括AltaRica基本語法結構、語義特征以及用衛(wèi)士轉換系統(tǒng)定義的形式化語義。(2)針對系統(tǒng)需求與設計模型之間的轉換問題,本文研究了四變量模型與AltaRica模型之間的語義映射規(guī)則。基于四變量模型與AltaRica模型的形式化語義構建了二者之間的語義映射,包括四類變量與AltaRica中的流變量和狀態(tài)變量等之間的映射以及四類關系與AltaRica中的斷言等結構之間的映射。基于該映射規(guī)則,可實現(xiàn)從四變量需求模型到AltaRica設計模型之間的轉換。(3)設計了一種從系統(tǒng)需求分析到模型設計的安全性分析驗證框架。首先,利用四變量模型從需求層面上對系統(tǒng)進行需求分析。然后,結合四變量模型與AltaRica模型之間的語義映射規(guī)則,利用AltaRica建模語言對系統(tǒng)進行模型設計,并基于AltaRica規(guī)則構建系統(tǒng)安全性屬性,最后對設計出的模型展開安全性分析和驗證。(4)給出了基于上述方法的民用飛機中機輪剎車系統(tǒng)的安全性實例分析。包括對其構建四變量模型、基于四變量模型與AltaRica模型間的語義映射規(guī)則進行AltaRica模型設計、基于AltaRica模型構建故障樹、利用相關工具對系統(tǒng)安全性進行分析并對安全性屬性進行驗證等。
【關鍵詞】：嵌入式系統(tǒng)設計 系統(tǒng)安全性分析 四變量模型 AltaRica SCR方法 故障樹
【學位授予單位】：南京航空航天大學
【學位級別】：碩士
【學位授予年份】：2016
【分類號】：V227;TP368.1
【目錄】：

• 摘要4-5
• ABSTRACT5-12
• 縮略詞12-13
• 第一章 緒論13-18
• 1.1 課題研究背景及意義13-14
• 1.2 當前研究現(xiàn)狀14-15
• 1.3 論文研究內容與論文結構15-18
• 第二章 基于模型的系統(tǒng)安全性分析概述18-29
• 2.1 模型驅動系統(tǒng)工程18-21
• 2.1.1 系統(tǒng)工程概述18-19
• 2.1.2 模型驅動工程19-21
• 2.2 傳統(tǒng)的安全性分析方法21-24
• 2.2.1 故障樹分析方法21-23
• 2.2.2 故障模式及影響分析方法23-24
• 2.3 基于模型的系統(tǒng)安全性分析24-27
• 2.3.1 面向需求的四變量模型25
• 2.3.2 面向設計的AltaRica模型25-27
• 2.4 從需求分析到模型設計的系統(tǒng)安全性分析驗證框架27-28
• 2.5 本章小結28-29
• 第三章 基于四變量模型的系統(tǒng)需求建模29-42
• 3.1 四變量模型概述29-32
• 3.1.1 關系REQ與關系NAT29-31
• 3.1.2 關系IN與關系OUT31-32
• 3.1.3 需求層面的軟件行為定義32
• 3.2 SCR方法及形式化語義32-38
• 3.2.1 SCR基本結構33
• 3.2.2 基于SCR方法的實例分析33-34
• 3.2.3 SCR方法形式化語義34-38
• 3.3 四變量模型需求分析實例38-41
• 3.3.1 機輪剎車系統(tǒng)中的隔離閥建模39-40
• 3.3.2 機輪剎車系統(tǒng)中的選擇閥建模40-41
• 3.4 本章小結41-42
• 第四章 面向ALTARICA的模型轉換與系統(tǒng)設計建模42-54
• 4.1 AltaRica模型的形式化定義42-44
• 4.2 四變量模型與AltaRica模型的語義映射44-50
• 4.2.1 MV和CV與AltaRica之間的映射44-46
• 4.2.2 IV和OV與AltaRica之間的映射46-48
• 4.2.3 關系NAT與AltaRica之間的映射48
• 4.2.4 關系REQ與AltaRica之間的映射48-49
• 4.2.5 關系IN和OUT與AltaRica之間的映射49-50
• 4.2.6 四變量模型與AltaRica模型之間的映射框架50
• 4.3 模型轉換實例分析50-53
• 4.3.1 隔離閥的AltaRica模型設計51-52
• 4.3.2 選擇閥的AltaRica模型設計52-53
• 4.4 本章小結53-54
• 第五章 機輪剎車系統(tǒng)實例建模與安全性分析驗證54-71
• 5.1 機輪剎車系統(tǒng)(WBS)概述54-57
• 5.1.1 剎車系統(tǒng)控制單元(BSCU)55-56
• 5.1.2 WBS系統(tǒng)中的部件蓄壓閥56
• 5.1.3 WBS系統(tǒng)中的部件限量閥56-57
• 5.2 WBS系統(tǒng)需求的四變量模型分析57-59
• 5.2.1 BSCU子系統(tǒng)的四變量模型57-58
• 5.2.2 蓄壓閥的四變量模型58
• 5.2.3 限量閥的四變量模型58-59
• 5.2.4 WBS系統(tǒng)的四變量模型59
• 5.3 WBS系統(tǒng)的SCR表設計59-62
• 5.3.1 WBS系統(tǒng)的模式轉換表構造59-60
• 5.3.2 WBS系統(tǒng)的事件表構造60-61
• 5.3.3 WBS系統(tǒng)的條件表構造61-62
• 5.4 WBS系統(tǒng)的AltaRica設計模型62-66
• 5.4.1 BSCU子系統(tǒng)的AltaRica模型63
• 5.4.2 蓄壓閥的AltaRica模型63-64
• 5.4.3 限量閥的AltaRica模型64-65
• 5.4.4 WBS系統(tǒng)的AltaRica模型65-66
• 5.5 WBS系統(tǒng)安全性分析與驗證66-69
• 5.5.1 構建故障樹66-67
• 5.5.2 安全性屬性總結及驗證67-69
• 5.6 本章小節(jié)69-71
• 第六章 總結與展望71-73
• 6.1 總結71-72
• 6.2 展望72-73
• 參考文獻73-78
• 致謝78-79
• 在學期間的研究成果及發(fā)表的學術論文79

，

本文編號：932906