MBSA框架下的安全性建模與分析技術(shù)研究

1、MBSA框架下的安全性建?？蚣芟碌陌踩越Ｅc分析技術(shù)研究與分析技術(shù)研究答辯人：范基坪 ZY1314109指導(dǎo)教師：趙廷弟整理pptCONTENTS目目 錄錄1 1研究背景與意義研究背景與意義2 2研究內(nèi)容與目標(biāo)研究內(nèi)容與目標(biāo)3 3基于模型的安全性分析框架基于模型的安全性分析框架4 4基于基于AltaRica的系統(tǒng)公共模型的系統(tǒng)公共模型5 5基于模型檢查的系統(tǒng)形式化驗(yàn)證方法基于模型檢查的系統(tǒng)形式化驗(yàn)證方法6 6案例分析：飛行控制系統(tǒng)案例分析：飛行控制系統(tǒng)7 7總結(jié)與展望總結(jié)與展望8 8碩士期間取得學(xué)術(shù)成果碩士期間取得學(xué)術(shù)成果整理pptCONTENTS目目 錄錄1 1研究背景與意義研究背景與意義

2、2 2研究內(nèi)容與目標(biāo)研究內(nèi)容與目標(biāo)3 3基于模型的安全性分析框架基于模型的安全性分析框架4 4基于基于AltaRica的系統(tǒng)公共模型的系統(tǒng)公共模型5 5基于模型檢查的系統(tǒng)形式化驗(yàn)證方法基于模型檢查的系統(tǒng)形式化驗(yàn)證方法6 6案例分析：飛行控制系統(tǒng)案例分析：飛行控制系統(tǒng)7 7總結(jié)與展望總結(jié)與展望8 8碩士期間取得學(xué)術(shù)成果碩士期間取得學(xué)術(shù)成果整理ppt研究背景與意義當(dāng)前安全性分析方法的弊端基于模型的安全性分析MBSA123分析結(jié)果的一致性n 安全分析人員在全面了解系統(tǒng)前提下開展安全性工作n 實(shí)際過程中往往需要投入大量時(shí)間收集系統(tǒng)結(jié)構(gòu)信息與系統(tǒng)行為n 分析準(zhǔn)確性嚴(yán)重依賴分析人員技術(shù)能力，易出錯(cuò)分析結(jié)果

3、的重用性n 產(chǎn)品設(shè)計(jì)迭代導(dǎo)致整體安全性結(jié)論的變化，從而產(chǎn)生大量重復(fù)性工作對系統(tǒng)失效行為的表達(dá)能力n 針對安全關(guān)鍵系統(tǒng)軟硬件高度耦合的情況，如何建立以功能為核心的失效事件描述方法整理ppt研究背景與意義MBSA相比傳統(tǒng)安全性分析的優(yōu)點(diǎn)流程優(yōu)勢流程優(yōu)勢n 系統(tǒng)設(shè)計(jì)人員與安全分析人員使用相同的系統(tǒng)模型n 避免了由于系統(tǒng)理解不一致而產(chǎn)生的設(shè)計(jì)分析協(xié)調(diào)問題n 有助于提高安全分析的完整性、連續(xù)性與可追溯性分析優(yōu)勢分析優(yōu)勢n 基于模型開展分析，利用現(xiàn)有的自動分析算法（例如故障樹、FMEA表格生成算法、形式化方法），通過計(jì)算機(jī)實(shí)現(xiàn)自動的安全性分析n 減少安全性分析人員重復(fù)性工作，降低設(shè)計(jì)成本整理pptCONT

4、ENTS目目 錄錄1 1研究背景與意義研究背景與意義2 2研究內(nèi)容與目標(biāo)研究內(nèi)容與目標(biāo)3 3基于模型的安全性分析框架基于模型的安全性分析框架4 4基于基于AltaRica的系統(tǒng)公共模型的系統(tǒng)公共模型5 5基于模型檢查的系統(tǒng)形式化驗(yàn)證方法基于模型檢查的系統(tǒng)形式化驗(yàn)證方法6 6案例分析：飛行控制系統(tǒng)案例分析：飛行控制系統(tǒng)7 7總結(jié)與展望總結(jié)與展望8 8碩士期間取得學(xué)術(shù)成果碩士期間取得學(xué)術(shù)成果整理ppt研究內(nèi)容與目標(biāo)基于模型的安全性分析框架基于模型的安全性分析框架 傳統(tǒng)安全性分析基礎(chǔ)上的MBSA過程 建立基于模型的安全性分析框架基于模型檢查的系統(tǒng)形式化驗(yàn)證基于模型檢查的系統(tǒng)形式化驗(yàn)證 原理 &

5、; 工具 NuSMV建模方法 系統(tǒng)規(guī)范定義方法 仿真與形式化驗(yàn)證方法案例：飛控系統(tǒng)案例：飛控系統(tǒng) 電傳飛控計(jì)算機(jī)AltaRica功能模型 飛控系統(tǒng)橫滾控制功能NuSMV模型 仿真 & 形式化驗(yàn)證基于基于AltaRica的系統(tǒng)公共模型的系統(tǒng)公共模型 AltaRica模型框架 建模元素 時(shí)間機(jī)制 優(yōu)先級&同步關(guān)系 故障行為描述方式 故障行為建模過程整理pptCONTENTS目目 錄錄1 1研究背景與意義研究背景與意義2 2研究內(nèi)容與目標(biāo)研究內(nèi)容與目標(biāo)3 3基于模型的安全性分析框架基于模型的安全性分析框架4 4基于基于AltaRica的系統(tǒng)公共模型的系統(tǒng)公共模型5 5基于模型檢查的系

6、統(tǒng)形式化驗(yàn)證方法基于模型檢查的系統(tǒng)形式化驗(yàn)證方法6 6案例分析：飛行控制系統(tǒng)案例分析：飛行控制系統(tǒng)7 7總結(jié)與展望總結(jié)與展望8 8碩士期間取得學(xué)術(shù)成果碩士期間取得學(xué)術(shù)成果整理ppt基于模型的安全性分析框架ARP4754A / 4761 分析過程n 飛機(jī)/系統(tǒng)級功能危險(xiǎn)評估 主要飛行階段 飛機(jī)/系統(tǒng)級功能分析 功能交互清單 應(yīng)急與環(huán)境狀態(tài) 功能失效分析n 初步飛機(jī)/系統(tǒng)安全性評估 FTA/其他分析 定性定量目標(biāo)符合方法 研制保證等級確定 故障模式與相關(guān)概率計(jì)算總結(jié)n 飛機(jī)/系統(tǒng)安全性評估 FTA、DD、MA 概率計(jì)算 表明符合性和定量需求的信息 系統(tǒng)/設(shè)備研制保證等級 FMEA/FMES不斷迭代

7、的不斷迭代的FTA、FMEA、DAL定義等工作定義等工作整理ppt基于模型的安全性分析框架基于模型的安全性分析流程n 形式化安全性需求 安全性需求的獲取需要依靠傳統(tǒng)安全性評估中的各類方法（FHA等） 將安全性需求的文本語言描述轉(zhuǎn)化為時(shí)態(tài)邏輯（線性時(shí)態(tài)邏輯、計(jì)算樹邏輯、其他高階謂詞邏輯） 安全性分析評估圍繞模型與所關(guān)注的安全性需求展開 公共模型與安全性需求都需要轉(zhuǎn)化為形式化語言后開展分析/評估整理ppt基于模型的安全性分析框架基于模型的安全性分析流程n 名義系統(tǒng)建模 通過構(gòu)建被研制系統(tǒng)的形式化模型，描述系統(tǒng)在正常功能狀態(tài)下的行為過程 支持建模環(huán)境： Simulink/Stateflow SCAD

8、E/Lustre Cecilia OCAS、Simfian 失效模式建模 描述各層級失效模式、構(gòu)建影響關(guān)系 通用失效模式： 數(shù)字部件輸出不確定、翻轉(zhuǎn)、鎖死 機(jī)械部件功能狀態(tài) 更復(fù)雜的故障行為： 故障傳播 條件故障（故障時(shí)序關(guān)系）整理ppt基于模型的安全性分析框架基于模型的安全性分析流程n 模型擴(kuò)展 失效模型加入到名義系統(tǒng)模型中，描述系統(tǒng)在各種故障條件下的行為，得到的模型稱作擴(kuò)展系統(tǒng)模型由于模型擴(kuò)展難度隨系統(tǒng)復(fù)雜度不斷增加，形成另一種建模思路：直接失效行為建模n 直接失效行為建模：失效邏輯 直接描述部件輸入失效模式與輸出失效模式怎樣與內(nèi)在失效相聯(lián)系 失效邏輯建模目標(biāo)明確，適合系統(tǒng)早期基于功能的安

9、全性評估整理ppt基于模型的安全性分析框架基于模型的安全性分析流程n 模型轉(zhuǎn)換 構(gòu)建系統(tǒng)公共模型的建模語言，例如Lustre、Simulink/Stateflow，AADL，AltaRica，需要轉(zhuǎn)換為形式化方法所要求的建模語言，例如SMV、HyDI及各類自動機(jī)語言整理ppt基于模型的安全性分析框架基于模型的安全性分析流程n 模型評估驗(yàn)證 仿真： 控制模型內(nèi)失效狀態(tài)的激活，從而展現(xiàn)不同故障對系統(tǒng)功能的影響，進(jìn)行系統(tǒng)的初步分析以及動態(tài)運(yùn)行細(xì)節(jié)的挖掘 安全屬性證明： 模型檢查 利用模型檢查器證明系統(tǒng)的安全性屬性在擴(kuò)展系統(tǒng)模型內(nèi)能否保持如果證實(shí)屬性不正確，修改設(shè)計(jì)或放寬安全性要求，定義其他可接受的約

10、束 定理證明n 安全性結(jié)論輸出 FTA、FMEA整理ppt基于模型的安全性分析框架MBSA工程開展階段劃分n 四部分內(nèi)容構(gòu)成一個(gè)小的工作閉環(huán)，從而在完整的設(shè)計(jì)周期內(nèi)重復(fù)進(jìn)行，直至滿足最終系統(tǒng)要求整理ppt基于模型的安全性分析框架MBSA與ARP4754A/4761結(jié)合方式n AFHA/SFHA階段 飛機(jī)級、系統(tǒng)級的功能安全性要求基本確定 針對不同公共系統(tǒng)建模方法，將功能安全性要求以形式化命題形式表示 系統(tǒng)需求的分解與細(xì)化n PSSA階段 構(gòu)建以功能為對象的系統(tǒng)模型，定義功能失效狀態(tài) 模型初步評估，驗(yàn)證飛機(jī)級功能與初步研制要求 自上而下細(xì)化失效行為n SSA階段 自下而上完成綜合與驗(yàn)證工作 公共

11、模型基本符合系統(tǒng)真實(shí)設(shè)計(jì) 通過相應(yīng)工具開展完整仿真、形式化驗(yàn)證，將分析結(jié)果轉(zhuǎn)化為FTA、FMEA等整理pptCONTENTS目目 錄錄1 1研究背景與意義研究背景與意義2 2研究內(nèi)容與目標(biāo)研究內(nèi)容與目標(biāo)3 3基于模型的安全性分析框架基于模型的安全性分析框架4 4基于基于AltaRica的系統(tǒng)公共模型的系統(tǒng)公共模型5 5基于模型檢查的系統(tǒng)形式化驗(yàn)證方法基于模型檢查的系統(tǒng)形式化驗(yàn)證方法6 6案例分析：飛行控制系統(tǒng)案例分析：飛行控制系統(tǒng)7 7總結(jié)與展望總結(jié)與展望8 8碩士期間取得學(xué)術(shù)成果碩士期間取得學(xué)術(shù)成果整理ppt基于AltaRica的系統(tǒng)公共模型AltaRica模型要素n 理論基礎(chǔ)：約束自動機(jī)

12、系統(tǒng)遷移的集合，遷移形式： 標(biāo)準(zhǔn)七元組：有限/無限域，狀態(tài)/流變量，事件，遷移，斷言，初始(V)(V)eGV , , , , ,AD S F E T A In 主要建模元素 子節(jié)點(diǎn)(Sub) 狀態(tài)(State) 流(Flow) 事件(Event) 初始值(Init) 遷移(Trans) 斷言(Assert) 外部(Extern) 同步(Sync)n 層次化 節(jié)點(diǎn)逐層實(shí)例化實(shí)現(xiàn)層次化建模 Main節(jié)點(diǎn)，設(shè)備節(jié)點(diǎn)，部件節(jié)點(diǎn)整理ppt基于AltaRica的系統(tǒng)公共模型AltaRica模型要素n 部件節(jié)點(diǎn) 狀態(tài)變量：open（布爾型） 事件：Open, Close 流變量：f1, f2 遷移定義內(nèi)部變

13、化 斷言定義狀態(tài)變量與流變量關(guān)系n 運(yùn)行/時(shí)間機(jī)制 以事件為核心的時(shí)間機(jī)制 以事件為時(shí)間分界點(diǎn) 狀態(tài)變量改變流變量改變整理ppt基于AltaRica的系統(tǒng)公共模型AltaRica模型要素n 運(yùn)行/時(shí)間機(jī)制 以事件為核心的時(shí)間機(jī)制 以事件為時(shí)間分界點(diǎn) 狀態(tài)變量改變流變量改變n 設(shè)備節(jié)點(diǎn) 設(shè)備節(jié)點(diǎn)類似容器，將具有模塊關(guān)系的部件節(jié)點(diǎn)組合在一起，利用流變量、斷言、同步等描述部件關(guān)系 子節(jié)點(diǎn)：Switch，Producer，Consumer 利用流變量f, f1, f2構(gòu)成三個(gè)部件狀態(tài)聯(lián)系整理ppt基于AltaRica的系統(tǒng)公共模型AltaRica建模過程n AltaRica建模是一個(gè)由下而上的建模過程

14、，確定完整的模型節(jié)點(diǎn)框架后，構(gòu)建每個(gè)部件節(jié)點(diǎn)模型，定義輸入輸出，狀態(tài)，事件，遷移，完成所有部件節(jié)點(diǎn)后根據(jù)層級關(guān)系逐層定義設(shè)備節(jié)點(diǎn)直至Main節(jié)點(diǎn)整理ppt基于AltaRica的系統(tǒng)公共模型AltaRica建模過程n 明確系統(tǒng)結(jié)構(gòu)與部件劃分n 確定部件節(jié)點(diǎn)輸入輸出流變量n 定義系統(tǒng)正常狀態(tài)與正常事件n 定義系統(tǒng)失效狀態(tài)與失效事件n 定義正常、失效狀態(tài)遷移關(guān)系n 建立失效影響關(guān)系n 定義設(shè)備節(jié)點(diǎn)實(shí)例化與流變量n 定義同步關(guān)系與優(yōu)先級整理pptCONTENTS目目 錄錄1 1研究背景與意義研究背景與意義2 2研究內(nèi)容與目標(biāo)研究內(nèi)容與目標(biāo)3 3基于模型的安全性分析框架基于模型的安全性分析框架4 4基于

15、基于AltaRica的系統(tǒng)公共模型的系統(tǒng)公共模型5 5基于模型檢查的系統(tǒng)形式化驗(yàn)證方法基于模型檢查的系統(tǒng)形式化驗(yàn)證方法6 6案例分析：飛行控制系統(tǒng)案例分析：飛行控制系統(tǒng)7 7總結(jié)與展望總結(jié)與展望8 8碩士期間取得學(xué)術(shù)成果碩士期間取得學(xué)術(shù)成果整理ppt基于模型檢查的系統(tǒng)形式化驗(yàn)證方法利用模型檢查的目的n 公共系統(tǒng)模型（AltaRica）并不能支持直接的安全性分析與驗(yàn)證n 形式化方法是自動分析的主流，其中模型檢查相比另一種方法定理證明具有更高的自動程度與簡單性n 生成反例支持進(jìn)一步分析評估模型檢查原理n 目標(biāo)系統(tǒng)模型（現(xiàn)有某一類描述語言）n 待驗(yàn)證屬性n 確定系統(tǒng)描述是否滿足規(guī)范的驗(yàn)證方法整理pp

16、t基于模型檢查的系統(tǒng)形式化驗(yàn)證方法模型檢查原理n 目標(biāo)屬性：時(shí)態(tài)邏輯 線性時(shí)態(tài)邏輯（Linear Temporal Logic, LTL）n 目標(biāo)系統(tǒng)：Kripke結(jié)構(gòu) 五元組： 除根節(jié)點(diǎn)以外，每個(gè)節(jié)點(diǎn)僅有一個(gè)前端，可以訪問任意后端節(jié)點(diǎn)，構(gòu)成一顆無限深度的樹0, , ,MS SR L AP時(shí)態(tài)算子時(shí)態(tài)算子全稱全稱含義含義GGlobal未來所有狀態(tài)FFinal未來某個(gè)狀態(tài)XneXt下一個(gè)狀態(tài)UUntil直到都RRelease直到才WWeak弱直到整理ppt基于模型檢查的系統(tǒng)形式化驗(yàn)證方法模型檢查原理n 目標(biāo)系統(tǒng)：Kripke結(jié)構(gòu) 五元組： 除根節(jié)點(diǎn)以外，每個(gè)節(jié)點(diǎn)僅有一個(gè)前端，可以訪問任意后端節(jié)點(diǎn)

17、，構(gòu)成一顆無限深度的樹0, , ,MS SR L APn 目標(biāo)屬性：時(shí)態(tài)邏輯 線性時(shí)態(tài)邏輯（Linear Temporal Logic, LTL）時(shí)態(tài)算子時(shí)態(tài)算子全稱全稱含義含義GGlobal未來所有狀態(tài)FFinal未來某個(gè)狀態(tài)XneXt下一個(gè)狀態(tài)UUntil直到都RRelease直到才WWeak弱直到整理ppt基于模型檢查的系統(tǒng)形式化驗(yàn)證方法模型檢查原理n 目標(biāo)系統(tǒng)：Kripke結(jié)構(gòu) 五元組： 除根節(jié)點(diǎn)以外，每個(gè)節(jié)點(diǎn)僅有一個(gè)前端，可以訪問任意后端節(jié)點(diǎn)，構(gòu)成一顆無限深度的樹0, , ,MS SR L APn 目標(biāo)屬性：時(shí)態(tài)邏輯 線性時(shí)態(tài)邏輯（Linear Temporal Logic, LTL

18、） 計(jì)算樹時(shí)態(tài)邏輯（Computing Tree Logic, CTL） 路徑量詞E（至少存在一條路徑） 路徑量詞A（所有路徑） 時(shí)態(tài)運(yùn)算符（G、F、X、U，同LTL）時(shí)態(tài)算子時(shí)態(tài)算子全稱全稱含義含義GGlobal未來所有狀態(tài)FFinal未來某個(gè)狀態(tài)XneXt下一個(gè)狀態(tài)UUntil直到都整理ppt基于模型檢查的系統(tǒng)形式化驗(yàn)證方法 NuSMV系統(tǒng)建模方法n NuSMV模型結(jié)構(gòu) 模塊名稱 模塊名字， 輸入?yún)⒘?模塊定義 變量（Variable）VAR， IVAR 約束（Constraint）ASSIGN，TRANS，INIT，NEXT 規(guī)范（Specification）CTLSPEC，LTLSPE

19、C整理ppt基于模型檢查的系統(tǒng)形式化驗(yàn)證方法 NuSMV系統(tǒng)建模方法n 建模步驟 系統(tǒng)信息收集層次、接口關(guān)系，功能分類、工作模式合理抽象 模塊定義確定SMV模型所有模塊功能與部件兩個(gè)角度構(gòu)建SMV模塊 模塊接口定義根據(jù)功能或部件數(shù)量、結(jié)構(gòu)定義MODULE關(guān)系，輸入變量數(shù)與類型控制變量數(shù)量，約束狀態(tài)空間 模塊狀態(tài)轉(zhuǎn)移定義在每個(gè)MODULE內(nèi)ASSIGN句段定義功能或部件狀態(tài)初值、下一時(shí)刻狀態(tài)及轉(zhuǎn)移條件n 失效建模方式名義系統(tǒng)+失效模型直接失效行為建模名義模型失效模型擴(kuò)展模型整理ppt基于模型檢查的系統(tǒng)形式化驗(yàn)證方法 NuSMV系統(tǒng)建模方法n 系統(tǒng)規(guī)范定義 存在型規(guī)范系統(tǒng)運(yùn)行過程中存在某個(gè)滿足命題

20、 的狀態(tài)特定失效狀態(tài)，失效組合狀態(tài)，系統(tǒng)臨界狀態(tài) 遷移型規(guī)范系統(tǒng)運(yùn)行過程中存在某個(gè)狀態(tài)滿足命題 p，并且未來存在滿足q的狀態(tài)部件執(zhí)行操作的順序，失效發(fā)生的次序 互斥型規(guī)范系統(tǒng)不會同時(shí)處于狀態(tài) p和 q余度部件不能同時(shí)出現(xiàn)失效的情況( )EF p&EEF pFq!AG()pq n AltaRica與SMV語言轉(zhuǎn)換整理ppt基于模型檢查的系統(tǒng)形式化驗(yàn)證方法 NuSMV仿真與形式化驗(yàn)證n NuSMV用戶界面n 仿真pick_statesimulate仿真初始狀態(tài)整理ppt基于模型檢查的系統(tǒng)形式化驗(yàn)證方法 NuSMV仿真與形式化驗(yàn)證n NuSMV用戶界面n 仿真pick_statesimula

21、te整理ppt基于模型檢查的系統(tǒng)形式化驗(yàn)證方法 NuSMV仿真與形式化驗(yàn)證n NuSMV用戶界面n 形式化驗(yàn)證（反例生成）check_ctlspec / check_ltlspecshow_propertyLTL公式G(command - F state=busy)：TRUECTL公式AG(command - AG state=busy )：FALSELTL公式：G(command - F state=busy)只要command為真，未來一定存在狀態(tài)使得state=busyCTL公式：AG(command - AG state=busy )對所有路徑，始終存在只要command為真，未來狀態(tài)

22、始終滿足state=busy整理pptCONTENTS目目 錄錄1 1研究背景與意義研究背景與意義2 2研究內(nèi)容與目標(biāo)研究內(nèi)容與目標(biāo)3 3基于模型的安全性分析框架基于模型的安全性分析框架4 4基于基于AltaRica的系統(tǒng)公共模型的系統(tǒng)公共模型5 5基于模型檢查的系統(tǒng)形式化驗(yàn)證方法基于模型檢查的系統(tǒng)形式化驗(yàn)證方法6 6案例分析：飛行控制系統(tǒng)案例分析：飛行控制系統(tǒng)7 7總結(jié)與展望總結(jié)與展望8 8碩士期間取得學(xué)術(shù)成果碩士期間取得學(xué)術(shù)成果整理ppt案例：飛控系統(tǒng)電傳飛控系統(tǒng)整理ppt案例：飛控系統(tǒng)電傳飛控系統(tǒng)整理ppt案例：飛控系統(tǒng)電傳飛控計(jì)算機(jī)AltaRica模型n 節(jié)點(diǎn)構(gòu)成n 部件節(jié)點(diǎn)：板卡級例

23、：EFCS板狀態(tài)遷移關(guān)系狀態(tài)遷移關(guān)系整理ppt案例：飛控系統(tǒng)電傳飛控計(jì)算機(jī)AltaRica模型n 節(jié)點(diǎn)構(gòu)成n 設(shè)備節(jié)點(diǎn)：飛控計(jì)算機(jī)單機(jī)板卡節(jié)點(diǎn)板卡節(jié)點(diǎn)輸入輸出關(guān)系整理ppt案例：飛控系統(tǒng)電傳飛控計(jì)算機(jī)AltaRica模型n 節(jié)點(diǎn)構(gòu)成n 設(shè)備節(jié)點(diǎn)：單機(jī)組合定義工作模式定義子節(jié)點(diǎn)遷移規(guī)則事件同步整理ppt案例：飛控系統(tǒng)多工作模式下橫滾控制功能NuSMV模型n NuSMV模塊結(jié)構(gòu)整理ppt案例：飛控系統(tǒng)多工作模式下橫滾控制功能NuSMV模型n 飛控計(jì)算機(jī)板級NuSMV模型n 飛控計(jì)算機(jī)單機(jī)模型定義狀態(tài)空間狀態(tài)遷移規(guī)則失效計(jì)數(shù)（PFCS/EFCS轉(zhuǎn)換）實(shí)例化子模塊單機(jī)級狀態(tài)遷移規(guī)則定義故障狀態(tài)整理ppt案例：飛控系統(tǒng)NuSMV模型分析n 仿真：名義模型（無故障系統(tǒng)）橫滾功能正常PFC