《MBSA框架下的全性建模与分析技术研究》由会员分享，可在线阅读，更多相关《MBSA框架下的全性建模与分析技术研究（52页珍藏版）》请在金锄头文库上搜索。
1、MBSA框架下的安全性建模与分析技术研究答辩人：范基坪 ZY1314109指导教师：赵廷弟CONTENTS目 录1 1研究背景与意义2 2研究内容与目标3 3基于模型的安全性分析框架4 4基于AltaRica的系统公共模型5 5基于模型检查的系统形式化验证方法6 6案例分析：飞行控制系统7 7总结与展望8 8硕士期间取得学术成果CONTENTS目 录1 1研究背景与意义2 2研究内容与目标3 3基于模型的安全性分析框架4 4基于AltaRica的系统公共模型5 5基于模型检查的系统形式化验证方法6 6案例分析：飞行控制系统7 7总结与展望8 8硕士期间取得学术成果研究背景与意义当前安全性分析方
2、法的弊端基于模型的安全性分析MBSA123分析结果的一致性n安全分析人员在全面了解系统前提下开展安全性工作n实际过程中往往需要投入大量时间收集系统结构信息与系统行为n分析准确性严重依赖分析人员技术能力，易出错分析结果的重用性n产品设计迭代导致整体安全性结论的变化，从而产生大量重复性工作对系统失效行为的表达能力n针对安全关键系统软硬件高度耦合的情况，如何建立以功能为核心的失效事件描述方法研究背景与意义MBSA相比传统安全性分析的优点流程优势n系统设计人员与安全分析人员使用相同的系统模型n避免了由于系统理解不一致而产生的设计分析协调问题n有助于提高安全分析的完整性、连续性与可追溯性分析优势n基于模
3、型开展分析，利用现有的自动分析算法（例如故障树、FMEA表格生成算法、形式化方法），通过计算机实现自动的安全性分析n减少安全性分析人员重复性工作，降低设计成本CONTENTS目 录1 1研究背景与意义2 2研究内容与目标3 3基于模型的安全性分析框架4 4基于AltaRica的系统公共模型5 5基于模型检查的系统形式化验证方法6 6案例分析：飞行控制系统7 7总结与展望8 8硕士期间取得学术成果研究内容与目标基于模型的安全性分析框架传统安全性分析基础上的MBSA过程建立基于模型的安全性分析框架基于模型检查的系统形式化验证原理 & 工具NuSMV建模方法系统规范定义方法仿真与形式化验证方法案例：
4、飞控系统电传飞控计算机AltaRica功能模型飞控系统横滚控制功能NuSMV模型仿真 & 形式化验证基于AltaRica的系统公共模型AltaRica模型框架建模元素时间机制优先级&同步关系故障行为描述方式故障行为建模过程CONTENTS目 录1 1研究背景与意义2 2研究内容与目标3 3基于模型的安全性分析框架4 4基于AltaRica的系统公共模型5 5基于模型检查的系统形式化验证方法6 6案例分析：飞行控制系统7 7总结与展望8 8硕士期间取得学术成果基于模型的安全性分析框架ARP4754A / 4761 分析过程n飞机/系统级功能危险评估主要飞行阶段飞机/系统级功能分析功能交互清单应急
5、与环境状态功能失效分析n初步飞机/系统安全性评估FTA/其他分析定性定量目标符合方法研制保证等级确定故障模式与相关概率计算总结n飞机/系统安全性评估FTA、DD、MA概率计算表明符合性和定量需求的信息系统/设备研制保证等级FMEA/FMES不断迭代的FTA、FMEA、DAL定义等工作基于模型的安全性分析框架基于模型的安全性分析流程n形式化安全性需求安全性需求的获取需要依靠传统安全性评估中的各类方法（FHA等）将安全性需求的文本语言描述转化为时态逻辑（线性时态逻辑、计算树逻辑、其他高阶谓词逻辑）安全性分析评估围绕模型与所关注的安全性需求展开公共模型与安全性需求都需要转化为形式化语言后开展分析/评
6、估基于模型的安全性分析框架基于模型的安全性分析流程n名义系统建模通过构建被研制系统的形式化模型，描述系统在正常功能状态下的行为过程支持建模环境：Simulink/StateflowSCADE/LustreCecilia OCAS、Simfian失效模式建模描述各层级失效模式、构建影响关系通用失效模式：数字部件输出不确定、翻转、锁死机械部件功能状态更复杂的故障行为：故障传播条件故障（故障时序关系）基于模型的安全性分析框架基于模型的安全性分析流程n模型扩展失效模型加入到名义系统模型中，描述系统在各种故障条件下的行为，得到的模型称作扩展系统模型由于模型扩展难度随系统复杂度不断增加，形成另一种建模思路
7、：直接失效行为建模n直接失效行为建模：失效逻辑直接描述部件输入失效模式与输出失效模式怎样与内在失效相联系失效逻辑建模目标明确，适合系统早期基于功能的安全性评估基于模型的安全性分析框架基于模型的安全性分析流程n模型转换构建系统公共模型的建模语言，例如Lustre、Simulink/Stateflow，AADL，AltaRica，需要转换为形式化方法所要求的建模语言，例如SMV、HyDI及各类自动机语言基于模型的安全性分析框架基于模型的安全性分析流程n模型评估验证仿真：控制模型内失效状态的激活，从而展现不同故障对系统功能的影响，进行系统的初步分析以及动态运行细节的挖掘安全属性证明：模型检查 利用模
8、型检查器证明系统的安全性属性在扩展系统模型内能否保持如果证实属性不正确，修改设计或放宽安全性要求，定义其他可接受的约束定理证明n安全性结论输出FTA、FMEA基于模型的安全性分析框架MBSA工程开展阶段划分n四部分内容构成一个小的工作闭环，从而在完整的设计周期内重复进行，直至满足最终系统要求基于模型的安全性分析框架MBSA与ARP4754A/4761结合方式nAFHA/SFHA阶段飞机级、系统级的功能安全性要求基本确定针对不同公共系统建模方法，将功能安全性要求以形式化命题形式表示系统需求的分解与细化nPSSA阶段构建以功能为对象的系统模型，定义功能失效状态模型初步评估，验证飞机级功能与初步研制
9、要求自上而下细化失效行为nSSA阶段自下而上完成综合与验证工作公共模型基本符合系统真实设计通过相应工具开展完整仿真、形式化验证，将分析结果转化为FTA、FMEA等CONTENTS目 录1 1研究背景与意义2 2研究内容与目标3 3基于模型的安全性分析框架4 4基于AltaRica的系统公共模型5 5基于模型检查的系统形式化验证方法6 6案例分析：飞行控制系统7 7总结与展望8 8硕士期间取得学术成果基于AltaRica的系统公共模型AltaRica模型要素n理论基础：约束自动机系统迁移的集合，迁移形式：标准七元组：有限/无限域，状态/流变量，事件，迁移，断言，初始n主要建模元素子节点(Sub)
10、状态(State)流(Flow)事件(Event)初始值(Init)迁移(Trans)断言(Assert)外部(Extern)同步(Sync)n层次化节点逐层实例化实现层次化建模Main节点，设备节点，部件节点基于AltaRica的系统公共模型AltaRica模型要素n部件节点状态变量：open（布尔型）事件：Open, Close流变量：f1, f2迁移定义内部变化断言定义状态变量与流变量关系n运行/时间机制以事件为核心的时间机制以事件为时间分界点状态变量改变流变量改变基于AltaRica的系统公共模型AltaRica模型要素n运行/时间机制以事件为核心的时间机制以事件为时间分界点状态变量改
11、变流变量改变n设备节点设备节点类似容器，将具有模块关系的部件节点组合在一起，利用流变量、断言、同步等描述部件关系子节点：Switch，Producer，Consumer利用流变量f, f1, f2构成三个部件状态联系基于AltaRica的系统公共模型AltaRica建模过程nAltaRica建模是一个由下而上的建模过程，确定完整的模型节点框架后，构建每个部件节点模型，定义输入输出，状态，事件，迁移，完成所有部件节点后根据层级关系逐层定义设备节点直至Main节点基于AltaRica的系统公共模型AltaRica建模过程n明确系统结构与部件划分n确定部件节点输入输出流变量n定义系统正常状态与正常事
12、件n定义系统失效状态与失效事件n定义正常、失效状态迁移关系n建立失效影响关系n定义设备节点实例化与流变量n定义同步关系与优先级CONTENTS目 录1 1研究背景与意义2 2研究内容与目标3 3基于模型的安全性分析框架4 4基于AltaRica的系统公共模型5 5基于模型检查的系统形式化验证方法6 6案例分析：飞行控制系统7 7总结与展望8 8硕士期间取得学术成果基于模型检查的系统形式化验证方法利用模型检查的目的n公共系统模型（AltaRica）并不能支持直接的安全性分析与验证n形式化方法是自动分析的主流，其中模型检查相比另一种方法定理证明具有更高的自动程度与简单性n生成反例支持进一步分析评估
13、模型检查原理n目标系统模型（现有某一类描述语言）n待验证属性n确定系统描述是否满足规范的验证方法基于模型检查的系统形式化验证方法模型检查原理n目标属性：时态逻辑线性时态逻辑（Linear Temporal Logic, LTL）n目标系统：Kripke结构五元组：除根节点以外，每个节点仅有一个前端，可以访问任意后端节点，构成一颗无限深度的树时态算子全称含义GGlobal未来所有状态FFinal未来某个状态XneXt下一个状态UUntil直到都RRelease直到才WWeak弱直到基于模型检查的系统形式化验证方法模型检查原理n目标系统：Kripke结构五元组：除根节点以外，每个节点仅有一个前端，
14、可以访问任意后端节点，构成一颗无限深度的树n目标属性：时态逻辑线性时态逻辑（Linear Temporal Logic, LTL）时态算子全称含义GGlobal未来所有状态FFinal未来某个状态XneXt下一个状态UUntil直到都RRelease直到才WWeak弱直到基于模型检查的系统形式化验证方法模型检查原理n目标系统：Kripke结构五元组：除根节点以外，每个节点仅有一个前端，可以访问任意后端节点，构成一颗无限深度的树n目标属性：时态逻辑线性时态逻辑（Linear Temporal Logic, LTL）计算树时态逻辑（Computing Tree Logic, CTL）路径量词E（至
15、少存在一条路径）路径量词A（所有路径）时态运算符（G、F、X、U，同LTL）时态算子全称含义GGlobal未来所有状态FFinal未来某个状态XneXt下一个状态UUntil直到都基于模型检查的系统形式化验证方法 NuSMV系统建模方法nNuSMV模型结构模块名称模块名字， 输入参量模块定义变量（Variable）VAR， IVAR约束（Constraint）ASSIGN，TRANS，INIT，NEXT规范（Specification）CTLSPEC，LTLSPEC基于模型检查的系统形式化验证方法 NuSMV系统建模方法n建模步骤系统信息收集层次、接口关系，功能分类、工作模式合理抽象模块定义确
16、定SMV模型所有模块功能与部件两个角度构建SMV模块模块接口定义根据功能或部件数量、结构定义MODULE关系，输入变量数与类型控制变量数量，约束状态空间模块状态转移定义在每个MODULE内ASSIGN句段定义功能或部件状态初值、下一时刻状态及转移条件 n失效建模方式名义系统+失效模型直接失效行为建模名义模型失效模型扩展模型基于模型检查的系统形式化验证方法 NuSMV系统建模方法n系统规范定义存在型规范系统运行过程中存在某个满足命题 的状态特定失效状态，失效组合状态，系统临界状态迁移型规范系统运行过程中存在某个状态满足命题 p，并且未来存在满足q的状态部件执行操作的顺序，失效发生的次序互斥型规范
17、系统不会同时处于状态 p和 q余度部件不能同时出现失效的情况 nAltaRica与SMV语言转换 基于模型检查的系统形式化验证方法 NuSMV仿真与形式化验证nNuSMV用户界面n仿真pick_statesimulate仿真初始状态基于模型检查的系统形式化验证方法 NuSMV仿真与形式化验证nNuSMV用户界面n仿真pick_statesimulate基于模型检查的系统形式化验证方法 NuSMV仿真与形式化验证nNuSMV用户界面n形式化验证（反例生成）check_ctlspec / check_ltlspecshow_propertyLTL公式G(command - F state=busy
18、)：TRUECTL公式AG(command - AG state=busy )：FALSELTL公式：G(command - F state=busy)只要command为真，未来一定存在状态使得state=busyCTL公式：AG(command - AG state=busy )对所有路径，始终存在只要command为真，未来状态始终满足state=busyCONTENTS目 录1 1研究背景与意义2 2研究内容与目标3 3基于模型的安全性分析框架4 4基于AltaRica的系统公共模型5 5基于模型检查的系统形式化验证方法6 6案例分析：飞行控制系统7 7总结与展望8 8硕士期间取得学术
19、成果案例：飞控系统电传飞控系统案例：飞控系统电传飞控系统案例：飞控系统电传飞控计算机AltaRica模型n节点构成n部件节点：板卡级例：EFCS板状态迁移关系状态迁移关系案例：飞控系统电传飞控计算机AltaRica模型n节点构成n设备节点：飞控计算机单机板卡节点板卡节点输入输出关系案例：飞控系统电传飞控计算机AltaRica模型n节点构成n设备节点：单机组合定义工作模式定义子节点迁移规则事件同步案例：飞控系统多工作模式下横滚控制功能NuSMV模型nNuSMV模块结构案例：飞控系统多工作模式下横滚控制功能NuSMV模型n飞控计算机板级NuSMV模型n飞控计算机单机模型定义状态空间状态迁移规则失效
20、计数（PFCS/EFCS转换）实例化子模块单机级状态迁移规则定义故障状态案例：飞控系统NuSMV模型分析n仿真：名义模型（无故障系统）横滚功能正常PFCS飞行模式名义系统状态下系统可以一直处于正常工作状态，而不会发生功能的横滚功能的失效系统状态不再变化案例：飞控系统NuSMV模型分析n仿真：PFCS，EFCS，DDC模式切换PFCSDDC状态转移路径-State:1.16State:1.1State:1.1State:1. 6State:1. 9AF work_mode=DDC)-State:1. 75X work_mode=EFCS)TRUE无5当一台杆位移传感器失效时，系统可以继续运行AE
21、 (RVDT_1.status=failure|RVDT_2.status=failure-E X Roll_Function=normal)FALSE系统提前进入功能丧失状态，反例描述情况真实不存在6双余度交流电源失效后，永磁发电机能立即启动G (pws.dynamo_1.status=failure&pws. dynamo_2.status=failure)|(pws.rectifying_box.status=failure)-AX (pws.pmg.status=normal)TRUE无7当两台惯性测量组件同时进入失效模式是，系统能进入DDC模式AG (IMU_1.status=failure&IMU_2.status=failure)-AF work_mode=DDC)FALSE系统提前进入EFCS模式导致无法切换到DDC8电源板失效一定会导致单台主机失效G (ps1.status=failure)|(ps2.status=failure)-X status=failure)FALSE单台电源板失效不会导致整台主机失效9左右主桨舵机不会同一时刻一起失效E (left_servo=normal right_servo=normal)TRUE无
