《MBSA框架下的安全性建模与分析技术研究.ppt》由会员分享，可在线阅读，更多相关《MBSA框架下的安全性建模与分析技术研究.ppt（52页珍藏版）》请在金锄头文库上搜索。
1、MBSA框架下的安全性建模与分析技术研究 答辩人 范基坪ZY1314109 指导教师 赵廷弟 CONTENTS 目录 CONTENTS 目录 当前安全性分析方法的弊端 MBSA相比传统安全性分析的优点 CONTENTS 目录 CONTENTS 目录 ARP4754A 4761分析过程 飞机 系统级功能危险评估主要飞行阶段飞机 系统级功能分析功能交互清单应急与环境状态功能失效分析 初步飞机 系统安全性评估FTA 其他分析定性定量目标符合方法研制保证等级确定故障模式与相关概率计算总结 飞机 系统安全性评估FTA DD MA概率计算表明符合性和定量需求的信息系统 设备研制保证等级FMEA FMES
2、不断迭代的FTA FMEA DAL定义等工作 基于模型的安全性分析流程 形式化安全性需求安全性需求的获取需要依靠传统安全性评估中的各类方法 FHA等 将安全性需求的文本语言描述转化为时态逻辑 线性时态逻辑 计算树逻辑 其他高阶谓词逻辑 安全性分析评估围绕模型与所关注的安全性需求展开公共模型与安全性需求都需要转化为形式化语言后开展分析 评估 基于模型的安全性分析流程 名义系统建模通过构建被研制系统的形式化模型 描述系统在正常功能状态下的行为过程支持建模环境 Simulink StateflowSCADE LustreCeciliaOCAS Simfia 失效模式建模描述各层级失效模式 构建影响关
3、系通用失效模式 数字部件输出不确定 翻转 锁死机械部件功能状态更复杂的故障行为 故障传播条件故障 故障时序关系 基于模型的安全性分析流程 模型扩展失效模型加入到名义系统模型中 描述系统在各种故障条件下的行为 得到的模型称作扩展系统模型 由于模型扩展难度随系统复杂度不断增加 形成另一种建模思路 直接失效行为建模 直接失效行为建模 失效逻辑直接描述部件输入失效模式与输出失效模式怎样与内在失效相联系失效逻辑建模目标明确 适合系统早期基于功能的安全性评估 基于模型的安全性分析流程 模型转换构建系统公共模型的建模语言 例如Lustre Simulink Stateflow AADL AltaRica 需
4、要转换为形式化方法所要求的建模语言 例如SMV HyDI及各类自动机语言 基于模型的安全性分析流程 模型评估验证仿真 控制模型内失效状态的激活 从而展现不同故障对系统功能的影响 进行系统的初步分析以及动态运行细节的挖掘安全属性证明 模型检查利用模型检查器证明系统的安全性属性在扩展系统模型内能否保持如果证实属性不正确 修改设计或放宽安全性要求 定义其他可接受的约束定理证明 安全性结论输出FTA FMEA MBSA工程开展阶段划分 四部分内容构成一个小的工作闭环 从而在完整的设计周期内重复进行 直至满足最终系统要求 MBSA与ARP4754A 4761结合方式 AFHA SFHA阶段飞机级 系统级
5、的功能安全性要求基本确定针对不同公共系统建模方法 将功能安全性要求以形式化命题形式表示系统需求的分解与细化 PSSA阶段构建以功能为对象的系统模型 定义功能失效状态模型初步评估 验证飞机级功能与初步研制要求自上而下细化失效行为 SSA阶段自下而上完成综合与验证工作公共模型基本符合系统真实设计通过相应工具开展完整仿真 形式化验证 将分析结果转化为FTA FMEA等 CONTENTS 目录 AltaRica模型要素 理论基础 约束自动机系统迁移的集合 迁移形式 标准七元组 有限 无限域 状态 流变量 事件 迁移 断言 初始 层次化节点逐层实例化实现层次化建模Main节点 设备节点 部件节点 Alt
6、aRica模型要素 部件节点状态变量 open 布尔型 事件 Open Close流变量 f1 f2迁移定义内部变化断言定义状态变量与流变量关系 运行 时间机制以事件为核心的时间机制以事件为时间分界点状态变量改变 流变量改变 AltaRica模型要素 运行 时间机制以事件为核心的时间机制以事件为时间分界点状态变量改变 流变量改变 设备节点设备节点类似容器 将具有模块关系的部件节点组合在一起 利用流变量 断言 同步等描述部件关系子节点 Switch Producer Consumer利用流变量f f1 f2构成三个部件状态联系 AltaRica建模过程 AltaRica建模是一个由下而上的建模过
7、程 确定完整的模型节点框架后 构建每个部件节点模型 定义输入输出 状态 事件 迁移 完成所有部件节点后根据层级关系逐层定义设备节点直至Main节点 AltaRica建模过程 明确系统结构与部件划分 确定部件节点输入输出流变量 定义系统正常状态与正常事件 定义系统失效状态与失效事件 定义正常 失效状态迁移关系 建立失效影响关系 定义设备节点实例化与流变量 定义同步关系与优先级 CONTENTS 目录 利用模型检查的目的 公共系统模型 AltaRica 并不能支持直接的安全性分析与验证形式化方法是自动分析的主流 其中模型检查相比另一种方法 定理证明具有更高的自动程度与简单性生成反例支持进一步分析评
8、估 模型检查原理 目标系统模型 现有某一类描述语言 待验证属性确定系统描述是否满足规范的验证方法 模型检查原理 目标属性 时态逻辑线性时态逻辑 LinearTemporalLogic LTL 目标系统 Kripke结构五元组 除根节点以外 每个节点仅有一个前端 可以访问任意后端节点 构成一颗无限深度的树 模型检查原理 目标系统 Kripke结构五元组 除根节点以外 每个节点仅有一个前端 可以访问任意后端节点 构成一颗无限深度的树 目标属性 时态逻辑线性时态逻辑 LinearTemporalLogic LTL 模型检查原理 目标系统 Kripke结构五元组 除根节点以外 每个节点仅有一个前端 可
9、以访问任意后端节点 构成一颗无限深度的树 目标属性 时态逻辑线性时态逻辑 LinearTemporalLogic LTL 计算树时态逻辑 ComputingTreeLogic CTL 路径量词E 至少存在一条路径 路径量词A 所有路径 时态运算符 G F X U 同LTL NuSMV系统建模方法 NuSMV模型结构模块名称模块名字 输入参量模块定义变量 Variable VAR IVAR约束 Constraint ASSIGN TRANS INIT NEXT规范 Specification CTLSPEC LTLSPEC NuSMV系统建模方法 建模步骤系统信息收集层次 接口关系 功能分类 工
10、作模式合理抽象模块定义确定SMV模型所有模块功能与部件两个角度构建SMV模块模块接口定义根据功能或部件数量 结构定义MODULE关系 输入变量数与类型控制变量数量 约束状态空间模块状态转移定义在每个MODULE内ASSIGN句段定义功能或部件状态初值 下一时刻状态及转移条件 失效建模方式名义系统 失效模型直接失效行为建模 NuSMV系统建模方法 系统规范定义存在型规范系统运行过程中存在某个满足命题的状态特定失效状态 失效组合状态 系统临界状态迁移型规范系统运行过程中存在某个状态满足命题p 并且未来存在满足q的状态部件执行操作的顺序 失效发生的次序互斥型规范系统不会同时处于状态p和q余度部件不能
11、同时出现失效的情况 AltaRica与SMV语言转换 NuSMV仿真与形式化验证 NuSMV用户界面 仿真pick statesimulate 仿真初始状态 NuSMV仿真与形式化验证 NuSMV用户界面 仿真pick statesimulate NuSMV仿真与形式化验证 NuSMV用户界面 形式化验证 反例生成 check ctlspec check ltlspecshow property LTL公式G command Fstate busy TRUECTL公式AG command AGstate busy FALSE LTL公式 G command Fstate busy 只要comm
12、and为真 未来一定存在状态使得state busyCTL公式 AG command AGstate busy 对所有路径 始终存在只要command为真 未来状态始终满足state busy CONTENTS 目录 电传飞控系统 电传飞控系统 电传飞控计算机AltaRica模型 节点构成 部件节点 板卡级 例 EFCS板 状态迁移关系 电传飞控计算机AltaRica模型 节点构成 设备节点 飞控计算机单机 板卡节点 板卡节点输入输出关系 电传飞控计算机AltaRica模型 节点构成 设备节点 单机组合 定义工作模式 定义子节点 迁移规则 事件同步 多工作模式下横滚控制功能NuSMV模型 Nu
13、SMV模块结构 多工作模式下横滚控制功能NuSMV模型 飞控计算机板级NuSMV模型 飞控计算机单机模型 NuSMV模型分析 仿真 名义模型 无故障系统 NuSMV模型分析 仿真 PFCS EFCS DDC模式切换 PFCS DDC状态转移路径 PFCS EFCS状态转移路径 NuSMV模型分析 仿真 横滚控制失效 State 1 9 Roll Function maifunction NuSMV模型分析 形式化验证 验证属性 系统无故障情况下不会进入EFCS模式LTLSPECG work mode EFCS 系统无故障情况下不会进入DDC模式LTLSPECG work mode DDC 系统
14、总是能确保横滚控制正常LTLSPECGRoll Function malfunction 形式化验证输出 NuSMV模型分析 形式化验证 验证属性 系统无故障情况下不会进入EFCS模式LTLSPECG work mode EFCS 系统无故障情况下不会进入DDC模式LTLSPECG work mode DDC 系统总是能确保横滚控制正常LTLSPECGRoll Function malfunction 验证属性 当两台惯性测量组件同时进入失效模式时 系统能进入DDC模式CTLSPECAG IMU 1 status failure IMU 2 status failure AFwork mode
15、 DDC CONTENTS 目录 主要研究成果 跟踪新版AltaRica AltaRica3 0 提高公共模型描述能力 NuSMV定量分析能力较弱 尝试开展概率模型检查 MBSA源于计算机科学 需进一步阐述模型检查理论与安全科学的关系 进一步研究的点 CONTENTS 目录 1 范基坪 焦健 赵海涛等 导航卫星单粒子软错误影响建模与仿真方法 J 北京航空航天大学学报 2015 2 FanJiping TingdiZhao JianJiao DispatchreliabilityofcivilaviationsimulationbasedonGeneralizedStochasticPetrin
16、ets GSPN C Guangzhou China InstituteofElectricalandElectronicsEngineersInc 2014 1033 1038 3 FanJiping JiaoJian WuWenbo AModel CheckingOrientedModelingMethodforSafetyCriticalSystem C Beijing 2015 4 FanJiping JiaoJian ZhanWen DispatchReleaseModelingandReliabilitySimulationinCivilAviation aGSPNApproach C GuangZhou China 2015 EI EI EI EI 5 ChenLu JiaoJian FanJiping AFaultPropagationModelingandAnalysisMethodBasedonModelChecking C Beijing 2015 第三作者 6 WeiQianxin JiaoJian FanJiping AnOptimizedMethodforG
