MBSA框架下的安全性建模与分析技术研究.ppt
《MBSA框架下的安全性建模与分析技术研究.ppt》由会员分享,可在线阅读,更多相关《MBSA框架下的安全性建模与分析技术研究.ppt(52页珍藏版)》请在三一文库上搜索。
1、MBSA框架下的安全性建模 与分析技术研究,答辩人:范基坪 ZY1314109,指导教师:赵廷弟,CONTENTS,目 录,CONTENTS,目 录,当前安全性分析方法的弊端,MBSA相比传统安全性分析的优点,CONTENTS,目 录,CONTENTS,目 录,ARP4754A / 4761 分析过程,飞机/系统级功能危险评估 主要飞行阶段 飞机/系统级功能分析 功能交互清单 应急与环境状态 功能失效分析,初步飞机/系统安全性评估 FTA/其他分析 定性定量目标符合方法 研制保证等级确定 故障模式与相关概率计算总结,飞机/系统安全性评估 FTA、DD、MA 概率计算 表明符合性和定量需求的信息
2、 系统/设备研制保证等级 FMEA/FMES,不断迭代的FTA、FMEA、DAL定义等工作,基于模型的安全性分析流程,形式化安全性需求 安全性需求的获取需要依靠传统安全性评估中的各类方法(FHA等) 将安全性需求的文本语言描述转化为时态逻辑(线性时态逻辑、计算树逻辑、其他高阶谓词逻辑),安全性分析评估围绕模型与所关注的安全性需求展开 公共模型与安全性需求都需要转化为形式化语言后开展分析/评估,基于模型的安全性分析流程,名义系统建模 通过构建被研制系统的形式化模型,描述系统在正常功能状态下的行为过程 支持建模环境: Simulink/Stateflow SCADE/Lustre Cecilia
3、OCAS、Simfia,失效模式建模 描述各层级失效模式、构建影响关系 通用失效模式: 数字部件输出不确定、翻转、锁死 机械部件功能状态 更复杂的故障行为: 故障传播 条件故障(故障时序关系),基于模型的安全性分析流程,模型扩展 失效模型加入到名义系统模型中,描述系统在各种故障条件下的行为,得到的模型称作扩展系统模型,由于模型扩展难度随系统复杂度不断增加,形成另一种建模思路:直接失效行为建模,直接失效行为建模:失效逻辑 直接描述部件输入失效模式与输出失效模式怎样与内在失效相联系 失效逻辑建模目标明确,适合系统早期基于功能的安全性评估,基于模型的安全性分析流程,模型转换 构建系统公共模型的建模语
4、言,例如Lustre、Simulink/Stateflow,AADL,AltaRica,需要转换为形式化方法所要求的建模语言,例如SMV、HyDI及各类自动机语言,基于模型的安全性分析流程,模型评估验证 仿真: 控制模型内失效状态的激活,从而展现不同故障对系统功能的影响,进行系统的初步分析以及动态运行细节的挖掘 安全属性证明: 模型检查 利用模型检查器证明系统的安全性属性在扩展系统模型内能否保持 如果证实属性不正确,修改设计或放宽安全性要求,定义其他可接受的约束 定理证明,安全性结论输出 FTA、FMEA,MBSA工程开展阶段划分,四部分内容构成一个小的工作闭环,从而在完整的设计周期内重复进行
5、,直至满足最终系统要求,MBSA与ARP4754A/4761结合方式,AFHA/SFHA阶段 飞机级、系统级的功能安全性要求基本确定 针对不同公共系统建模方法,将功能安全性要求以形式化命题形式表示 系统需求的分解与细化,PSSA阶段 构建以功能为对象的系统模型,定义功能失效状态 模型初步评估,验证飞机级功能与初步研制要求 自上而下细化失效行为,SSA阶段 自下而上完成综合与验证工作 公共模型基本符合系统真实设计 通过相应工具开展完整仿真、形式化验证,将分析结果转化为FTA、FMEA等,CONTENTS,目 录,AltaRica模型要素,理论基础:约束自动机 系统迁移的集合,迁移形式: 标准七元
6、组: 有限/无限域,状态/流变量,事件,迁移, 断言,初始,层次化 节点逐层实例化实现层次化建模 Main节点,设备节点,部件节点,AltaRica模型要素,部件节点 状态变量:open(布尔型) 事件:Open, Close 流变量:f1, f2 迁移定义内部变化 断言定义状态变量与流变量关系,运行/时间机制 以事件为核心的时间机制 以事件为时间分界点 状态变量改变流变量改变,AltaRica模型要素,运行/时间机制 以事件为核心的时间机制 以事件为时间分界点 状态变量改变流变量改变,设备节点 设备节点类似容器,将具有模块关系的部件节点组合在一起,利用流变量、断言、同步等描述部件关系 子节点
7、:Switch,Producer,Consumer 利用流变量f, f1, f2构成三个部件状态联系,AltaRica建模过程,AltaRica建模是一个由下而上的建模过程,确定完整的模型节点框架后,构建每个部件节点模型,定义输入输出,状态,事件,迁移,完成所有部件节点后根据层级关系逐层定义设备节点直至Main节点,AltaRica建模过程,明确系统结构与部件划分,确定部件节点输入输出流变量,定义系统正常状态与正常事件,定义系统失效状态与失效事件,定义正常、失效状态迁移关系,建立失效影响关系,定义设备节点实例化与流变量,定义同步关系与优先级,CONTENTS,目 录,利用模型检查的目的,公共系
8、统模型(AltaRica)并不能支持直接的安全性分析与验证 形式化方法是自动分析的主流,其中模型检查相比另一种方法定理证明具有更高的自动程度与简单性 生成反例支持进一步分析评估,模型检查原理,目标系统模型(现有某一类描述语言) 待验证属性 确定系统描述是否满足规范的验证方法,模型检查原理,目标属性:时态逻辑 线性时态逻辑(Linear Temporal Logic, LTL),目标系统:Kripke结构 五元组: 除根节点以外,每个节点仅有一个前端,可以访问任意后端节点,构成一颗无限深度的树,模型检查原理,目标系统:Kripke结构 五元组: 除根节点以外,每个节点仅有一个前端,可以访问任意后
9、端节点,构成一颗无限深度的树,目标属性:时态逻辑 线性时态逻辑(Linear Temporal Logic, LTL),模型检查原理,目标系统:Kripke结构 五元组: 除根节点以外,每个节点仅有一个前端,可以访问任意后端节点,构成一颗无限深度的树,目标属性:时态逻辑 线性时态逻辑(Linear Temporal Logic, LTL) 计算树时态逻辑(Computing Tree Logic, CTL) 路径量词E(至少存在一条路径) 路径量词A(所有路径) 时态运算符(G、F、X、U,同LTL),NuSMV系统建模方法,NuSMV模型结构 模块名称 模块名字, 输入参量 模块定义 变量(
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- MBSA 框架 安全性 建模 分析 技术研究
链接地址:https://www.31doc.com/p-3575320.html