《MBSA框架下的安全性建模与分析技术研究.ppt》由会员分享，可在线阅读，更多相关《MBSA框架下的安全性建模与分析技术研究.ppt（52页珍藏版）》请在三一办公上搜索。
1、MBSA框架下的安全性建模与分析技术研究,答辩人：范基坪 ZY1314109,指导教师：赵廷弟,CONTENTS,目 录,CONTENTS,目 录,当前安全性分析方法的弊端,MBSA相比传统安全性分析的优点,CONTENTS,目 录,CONTENTS,目 录,ARP4754A/4761 分析过程,飞机/系统级功能危险评估主要飞行阶段飞机/系统级功能分析功能交互清单应急与环境状态功能失效分析,初步飞机/系统安全性评估FTA/其他分析定性定量目标符合方法研制保证等级确定故障模式与相关概率计算总结,飞机/系统安全性评估FTA、DD、MA概率计算表明符合性和定量需求的信息系统/设备研制保证等级FMEA
2、/FMES,不断迭代的FTA、FMEA、DAL定义等工作,基于模型的安全性分析流程,形式化安全性需求安全性需求的获取需要依靠传统安全性评估中的各类方法（FHA等）将安全性需求的文本语言描述转化为时态逻辑（线性时态逻辑、计算树逻辑、其他高阶谓词逻辑）,安全性分析评估围绕模型与所关注的安全性需求展开公共模型与安全性需求都需要转化为形式化语言后开展分析/评估,基于模型的安全性分析流程,名义系统建模通过构建被研制系统的形式化模型，描述系统在正常功能状态下的行为过程支持建模环境：Simulink/StateflowSCADE/LustreCecilia OCAS、Simfia,失效模式建模描述各层级失效
3、模式、构建影响关系通用失效模式：数字部件输出不确定、翻转、锁死机械部件功能状态更复杂的故障行为：故障传播条件故障（故障时序关系）,基于模型的安全性分析流程,模型扩展失效模型加入到名义系统模型中，描述系统在各种故障条件下的行为，得到的模型称作扩展系统模型,由于模型扩展难度随系统复杂度不断增加，形成另一种建模思路：直接失效行为建模,直接失效行为建模：失效逻辑直接描述部件输入失效模式与输出失效模式怎样与内在失效相联系失效逻辑建模目标明确，适合系统早期基于功能的安全性评估,基于模型的安全性分析流程,模型转换构建系统公共模型的建模语言，例如Lustre、Simulink/Stateflow，AADL，A
4、ltaRica，需要转换为形式化方法所要求的建模语言，例如SMV、HyDI及各类自动机语言,基于模型的安全性分析流程,模型评估验证仿真：控制模型内失效状态的激活，从而展现不同故障对系统功能的影响，进行系统的初步分析以及动态运行细节的挖掘安全属性证明：模型检查 利用模型检查器证明系统的安全性属性在扩展系统模型内能否保持如果证实属性不正确，修改设计或放宽安全性要求，定义其他可接受的约束定理证明,安全性结论输出FTA、FMEA,MBSA工程开展阶段划分,四部分内容构成一个小的工作闭环，从而在完整的设计周期内重复进行，直至满足最终系统要求,MBSA与ARP4754A/4761结合方式,AFHA/SFH
5、A阶段飞机级、系统级的功能安全性要求基本确定针对不同公共系统建模方法，将功能安全性要求以形式化命题形式表示系统需求的分解与细化,PSSA阶段构建以功能为对象的系统模型，定义功能失效状态模型初步评估，验证飞机级功能与初步研制要求自上而下细化失效行为,SSA阶段自下而上完成综合与验证工作公共模型基本符合系统真实设计通过相应工具开展完整仿真、形式化验证，将分析结果转化为FTA、FMEA等,CONTENTS,目 录,AltaRica模型要素,理论基础：约束自动机系统迁移的集合，迁移形式：标准七元组：有限/无限域，状态/流变量，事件，迁移，断言，初始,层次化节点逐层实例化实现层次化建模Main节点，设备
6、节点，部件节点,AltaRica模型要素,部件节点状态变量：open（布尔型）事件：Open,Close流变量：f1,f2迁移定义内部变化断言定义状态变量与流变量关系,运行/时间机制以事件为核心的时间机制以事件为时间分界点状态变量改变流变量改变,AltaRica模型要素,运行/时间机制以事件为核心的时间机制以事件为时间分界点状态变量改变流变量改变,设备节点设备节点类似容器，将具有模块关系的部件节点组合在一起，利用流变量、断言、同步等描述部件关系子节点：Switch，Producer，Consumer利用流变量f,f1,f2构成三个部件状态联系,AltaRica建模过程,AltaRica建模是一
7、个由下而上的建模过程，确定完整的模型节点框架后，构建每个部件节点模型，定义输入输出，状态，事件，迁移，完成所有部件节点后根据层级关系逐层定义设备节点直至Main节点,AltaRica建模过程,明确系统结构与部件划分,确定部件节点输入输出流变量,定义系统正常状态与正常事件,定义系统失效状态与失效事件,定义正常、失效状态迁移关系,建立失效影响关系,定义设备节点实例化与流变量,定义同步关系与优先级,CONTENTS,目 录,利用模型检查的目的,公共系统模型（AltaRica）并不能支持直接的安全性分析与验证形式化方法是自动分析的主流，其中模型检查相比另一种方法定理证明具有更高的自动程度与简单性生成反
8、例支持进一步分析评估,模型检查原理,目标系统模型（现有某一类描述语言）待验证属性确定系统描述是否满足规范的验证方法,模型检查原理,目标属性：时态逻辑线性时态逻辑（Linear Temporal Logic,LTL）,目标系统：Kripke结构五元组：除根节点以外，每个节点仅有一个前端，可以访问任意后端节点，构成一颗无限深度的树,模型检查原理,目标系统：Kripke结构五元组：除根节点以外，每个节点仅有一个前端，可以访问任意后端节点，构成一颗无限深度的树,目标属性：时态逻辑线性时态逻辑（Linear Temporal Logic,LTL）,模型检查原理,目标系统：Kripke结构五元组：除根节点
9、以外，每个节点仅有一个前端，可以访问任意后端节点，构成一颗无限深度的树,目标属性：时态逻辑线性时态逻辑（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系统建模方法,建模步骤
10、系统信息收集层次、接口关系，功能分类、工作模式合理抽象模块定义确定SMV模型所有模块功能与部件两个角度构建SMV模块模块接口定义根据功能或部件数量、结构定义MODULE关系，输入变量数与类型控制变量数量，约束状态空间模块状态转移定义在每个MODULE内ASSIGN句段定义功能或部件状态初值、下一时刻状态及转移条件,失效建模方式名义系统+失效模型直接失效行为建模,NuSMV系统建模方法,系统规范定义存在型规范系统运行过程中存在某个满足命题 的状态特定失效状态，失效组合状态，系统临界状态迁移型规范系统运行过程中存在某个状态满足命题 p，并且未来存在满足q的状态部件执行操作的顺序，失效发生的次序互斥
11、型规范系统不会同时处于状态 p和 q余度部件不能同时出现失效的情况,AltaRica与SMV语言转换,NuSMV仿真与形式化验证,NuSMV用户界面,仿真pick_statesimulate,仿真初始状态,NuSMV仿真与形式化验证,NuSMV用户界面,仿真pick_statesimulate,NuSMV仿真与形式化验证,NuSMV用户界面,形式化验证（反例生成）check_ctlspec/check_ltlspecshow_property,LTL公式G(command-F state=busy)：TRUECTL公式AG(command-AG state=busy)：FALSE,LTL公式：
12、G(command-F state=busy)只要command为真，未来一定存在状态使得state=busyCTL公式：AG(command-AG state=busy)对所有路径，始终存在只要command为真，未来状态始终满足state=busy,CONTENTS,目 录,电传飞控系统,电传飞控系统,电传飞控计算机AltaRica模型,节点构成,部件节点：板卡级,例：EFCS板,状态迁移关系,电传飞控计算机AltaRica模型,节点构成,设备节点：飞控计算机单机,板卡节点,板卡节点输入输出关系,电传飞控计算机AltaRica模型,节点构成,设备节点：单机组合,定义工作模式,定义子节点,迁
13、移规则,事件同步,多工作模式下横滚控制功能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);-系统无故障
14、情况下不会进入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模
15、式 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.Dispat
16、ch reliability of civil aviation simulation based on Generalized Stochastic Petri nets(GSPN)C.Guangzhou,China、:Institute of Electrical and Electronics Engineers Inc.，2014:1033-10383Fan Jiping,Jiao Jian,Wu Wenbo.A Model-Checking Oriented Modeling Method for Safety Critical SystemC.Beijing，20154 Fan J
17、iping,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（第三作者）,感谢聆听,请各位老师批评指正！,
