MBSA框架下的安全性建模与分析技术研究.ppt

MBSA框架下的安全性建模 与分析技术研究,答辩人：范基坪 ZY1314109,指导教师：赵廷弟,CONTENTS,目 录,CONTENTS,目 录,当前安全性分析方法的弊端,MBSA相比传统安全性分析的优点,CONTENTS,目 录,CONTENTS,目 录,ARP4754A / 4761 分析过程,飞机/系统级功能危险评估 主要飞行阶段 飞机/系统级功能分析 功能交互清单 应急与环境状态 功能失效分析,初步飞机/系统安全性评估 FTA/其他分析 定性定量目标符合方法 研制保证等级确定 故障模式与相关概率计算总结,飞机/系统安全性评估 FTA、DD、MA 概率计算 表明符合性和定量需求的信息 系统/设备研制保证等级 FMEA/FMES,不断迭代的FTA、FMEA、DAL定义等工作,基于模型的安全性分析流程,形式化安全性需求 安全性需求的获取需要依靠传统安全性评估中的各类方法（FHA等） 将安全性需求的文本语言描述转化为时态逻辑（线性时态逻辑、计算树逻辑、其他高阶谓词逻辑）,安全性分析评估围绕模型与所关注的安全性需求展开 公共模型与安全性需求都需要转化为形式化语言后开展分析/评估,基于模型的安全性分析流程,名义系统建模 通过构建被研制系统的形式化模型，描述系统在正常功能状态下的行为过程 支持建模环境： Simulink/Stateflow SCADE/Lustre Cecilia OCAS、Simfia,失效模式建模 描述各层级失效模式、构建影响关系 通用失效模式： 数字部件输出不确定、翻转、锁死 机械部件功能状态 更复杂的故障行为： 故障传播 条件故障（故障时序关系）,基于模型的安全性分析流程,模型扩展 失效模型加入到名义系统模型中，描述系统在各种故障条件下的行为，得到的模型称作扩展系统模型,由于模型扩展难度随系统复杂度不断增加，形成另一种建模思路：直接失效行为建模,直接失效行为建模：失效逻辑 直接描述部件输入失效模式与输出失效模式怎样与内在失效相联系 失效逻辑建模目标明确，适合系统早期基于功能的安全性评估,基于模型的安全性分析流程,模型转换 构建系统公共模型的建模语言，例如Lustre、Simulink/Stateflow，AADL，AltaRica，需要转换为形式化方法所要求的建模语言，例如SMV、HyDI及各类自动机语言,基于模型的安全性分析流程,模型评估验证 仿真： 控制模型内失效状态的激活，从而展现不同故障对系统功能的影响，进行系统的初步分析以及动态运行细节的挖掘 安全属性证明： 模型检查 利用模型检查器证明系统的安全性属性在扩展系统模型内能否保持 如果证实属性不正确，修改设计或放宽安全性要求，定义其他可接受的约束 定理证明,安全性结论输出 FTA、FMEA,MBSA工程开展阶段划分,四部分内容构成一个小的工作闭环，从而在完整的设计周期内重复进行，直至满足最终系统要求,MBSA与ARP4754A/4761结合方式,AFHA/SFHA阶段 飞机级、系统级的功能安全性要求基本确定 针对不同公共系统建模方法，将功能安全性要求以形式化命题形式表示 系统需求的分解与细化,PSSA阶段 构建以功能为对象的系统模型，定义功能失效状态 模型初步评估，验证飞机级功能与初步研制要求 自上而下细化失效行为,SSA阶段 自下而上完成综合与验证工作 公共模型基本符合系统真实设计 通过相应工具开展完整仿真、形式化验证，将分析结果转化为FTA、FMEA等,CONTENTS,目 录,AltaRica模型要素,理论基础：约束自动机 系统迁移的集合，迁移形式： 标准七元组： 有限/无限域，状态/流变量，事件，迁移， 断言，初始,层次化 节点逐层实例化实现层次化建模 Main节点，设备节点，部件节点,AltaRica模型要素,部件节点 状态变量：open（布尔型） 事件：Open, Close 流变量：f1, f2 迁移定义内部变化 断言定义状态变量与流变量关系,运行/时间机制 以事件为核心的时间机制 以事件为时间分界点 状态变量改变流变量改变,AltaRica模型要素,运行/时间机制 以事件为核心的时间机制 以事件为时间分界点 状态变量改变流变量改变,设备节点 设备节点类似容器，将具有模块关系的部件节点组合在一起，利用流变量、断言、同步等描述部件关系 子节点：Switch，Producer，Consumer 利用流变量f, f1, f2构成三个部件状态联系,AltaRica建模过程,AltaRica建模是一个由下而上的建模过程，确定完整的模型节点框架后，构建每个部件节点模型，定义输入输出，状态，事件，迁移，完成所有部件节点后根据层级关系逐层定义设备节点直至Main节点,AltaRica建模过程,明确系统结构与部件划分,确定部件节点输入输出流变量,定义系统正常状态与正常事件,定义系统失效状态与失效事件,定义正常、失效状态迁移关系,建立失效影响关系,定义设备节点实例化与流变量,定义同步关系与优先级,CONTENTS,目 录,利用模型检查的目的,公共系统模型（AltaRica）并不能支持直接的安全性分析与验证 形式化方法是自动分析的主流，其中模型检查相比另一种方法定理证明具有更高的自动程度与简单性 生成反例支持进一步分析评估,模型检查原理,目标系统模型（现有某一类描述语言） 待验证属性 确定系统描述是否满足规范的验证方法,模型检查原理,目标属性：时态逻辑 线性时态逻辑（Linear Temporal Logic, LTL）,目标系统：Kripke结构 五元组： 除根节点以外，每个节点仅有一个前端，可以访问任意后端节点，构成一颗无限深度的树,模型检查原理,目标系统：Kripke结构 五元组： 除根节点以外，每个节点仅有一个前端，可以访问任意后端节点，构成一颗无限深度的树,目标属性：时态逻辑 线性时态逻辑（Linear Temporal Logic, LTL）,模型检查原理,目标系统：Kripke结构 五元组： 除根节点以外，每个节点仅有一个前端，可以访问任意后端节点，构成一颗无限深度的树,目标属性：时态逻辑 线性时态逻辑（Linear Temporal Logic, LTL） 计算树时态逻辑（Computing Tree Logic, CTL） 路径量词E（至少存在一条路径） 路径量词A（所有路径） 时态运算符（G、F、X、U，同LTL）,NuSMV系统建模方法,NuSMV模型结构 模块名称 模块名字， 输入参量 模块定义 变量（Variable） VAR， IVAR 约束（Constraint） ASSIGN，TRANS，INIT，NEXT 规范（Specification） CTLSPEC，LTLSPEC,NuSMV系统建模方法,建模步骤 系统信息收集 层次、接口关系，功能分类、工作模式 合理抽象 模块定义 确定SMV模型所有模块 功能与部件两个角度构建SMV模块 模块接口定义 根据功能或部件数量、结构定义MODULE关系，输入变量数与类型 控制变量数量，约束状态空间 模块状态转移定义 在每个MODULE内ASSIGN句段定义功能或部件状态初值、下一时刻状态及转移条件,失效建模方式 名义系统+失效模型 直接失效行为建模,NuSMV系统建模方法,系统规范定义 存在型规范 系统运行过程中存在某个满足命题 的状态 特定失效状态，失效组合状态，系统临界状态 迁移型规范 系统运行过程中存在某个状态满足命题 p，并且未来存在满足q的状态 部件执行操作的顺序，失效发生的次序 互斥型规范 系统不会同时处于状态 p和 q 余度部件不能同时出现失效的情况,AltaRica与SMV语言转换,NuSMV仿真与形式化验证,NuSMV用户界面,仿真 pick_state simulate,仿真初始状态,NuSMV仿真与形式化验证,NuSMV用户界面,仿真 pick_state simulate,NuSMV仿真与形式化验证,NuSMV用户界面,形式化验证（反例生成） check_ctlspec / check_ltlspec show_property,LTL公式G(command - F state=busy)：TRUE CTL公式AG(command - AG state=busy )：FALSE,LTL公式：G(command - F state=busy) 只要command为真，未来一定存在状态使得state=busy CTL公式：AG(command - AG state=busy ) 对所有路径，始终存在只要command为真，未来状态始终满足state=busy,CONTENTS,目 录,电传飞控系统,电传飞控系统,电传飞控计算机AltaRica模型,节点构成,部件节点：板卡级,例：EFCS板,状态迁移关系,电传飞控计算机AltaRica模型,节点构成,设备节点：飞控计算机单机,板卡节点,板卡节点输入输出关系,电传飞控计算机AltaRica模型,节点构成,设备节点：单机组合,定义工作模式,定义子节点,迁移规则,事件同步,多工作模式下横滚控制功能NuSMV模型,NuSMV模块结构,多工作模式下横滚控制功能NuSMV模型,飞控计算机板级NuSMV模型,飞控计算机单机模型,NuSMV模型分析,仿真：名义模型（无故障系统）,NuSMV模型分析,仿真：PFCS，EFCS，DDC模式切换,PFCSDDC状态转移路径,PFCSEFCS状态转移路径,NuSMV模型分析,仿真：横滚控制失效,-State:1. 9- Roll_Function = maifunction,NuSMV模型分析,形式化验证,验证属性： -系统无故障情况下不会进入EFCS模式 LTLSPEC G (work_mode != EFCS); -系统无故障情况下不会进入DDC模式 LTLSPEC G (work_mode != DDC); -系统总是能确保横滚控制正常 LTLSPEC G Roll_Function!=malfunction;,形式化验证输出,NuSMV模型分析,形式化验证,验证属性： -系统无故障情况下不会进入EFCS模式 LTLSPEC G (work_mode != EFCS); -系统无故障情况下不会进入DDC模式 LTLSPEC G (work_mode != DDC); -系统总是能确保横滚控制正常 LTLSPEC G Roll_Function!=malfunction;,验证属性： -当两台惯性测量组件同时进入失效模式时，系统能进入DDC模式 CTLSPEC AG (IMU_1.status=failure&IMU_2.status=failure)-AF work_mode=DDC),CONTENTS,目 录,主要研究成果,跟踪新版AltaRicaAltaRica 3.0，提高公共模型描述能力,NuSMV定量分析能力较弱，尝试开展概率模型检查,MBSA源于计算机科学，需进一步阐述模型检查理论与安全科学的关系,进一步研究的点,CONTENTS,目 录,1 范基坪，焦健，赵海涛等. 导航卫星单粒子软错误影响建模与仿真方法J. 北京航空航天大学学报. 2015 2Fan Jiping, Tingdi Zhao, Jian Jiao. Dispatch reliability of civil aviation simulation based on Generalized Stochastic Petri nets (GSPN)C. Guangzhou, China、: Institute of Electrical and Electronics Engineers Inc.，2014: 1033-1038 3Fan Jiping, Jiao Jian, Wu Wenbo. A Model-Checking Oriented Modeling Method for Safety Critical SystemC. Beijing，2015 4 Fan Jiping, Jiao Jian, Zhan Wen. Dispatch Release Modeling and Reliability Simulation in Civil Aviation: a GSPN ApproachC. Guang Zhou, China，2015,EI,EI,EI,EI,5Chen Lu, Jiao Jian, Fan Jiping. A Fault Propagation Modeling and Analysis Method Based on Model CheckingC. Beijing，2015（第三作者） 6Wei Qianxin, Jiao Jian, Fan Jiping. An Optimized Method for Generating Fault Tree from Counter-exampleC. Tucson, AZ, USA，2016（第三作者） 7Chen Lu, Jiao Jian, Fan Jiping. A Fault Propagation Modeling and Analysis Method Based on Model CheckingC. Tucson, AZ, USA，2016（第三作者）,感谢聆听,请各位老师批评指正！,