安全关键系统需求形式化建模分析实例研究

论文摘要

近年来,基于模型的安全性分析技术(MBSA)在航空等领域有着广泛应用,因此对以xSAP安全分析平台为核心,基于MBSA的系统安全性评估方法进行了研究,并通过一个真实的综合航电系统Garmin G1000的自动飞行控制系统(AFCS)GFC700为实例来详细介绍。该方法的实现包括使用NuSMV形式化语言对系统进行需求建模,根据系统设计故障模式,在NuSMV模型中注入故障事件,使用xSAP对NuSMV需求模型进行模型扩展得到故障扩展模型,以及对故障扩展模型进行故障分析及系统安全性评估,例如生成故障树及FMEA表等。从分析结果来看,使用xSAP平台对实际系统进行基于模型的系统安全分析是行之有效的。

论文目录

• 1 引言
• 2 MBSA和形式化模型
•   2.1 基于模型的安全性分析方法
•   2.2 形式化建模与分析
• 3 基于形式化模型的系统安全性分析
•   3.1 基于形式化模型的系统安全性分析框架
•   3.2 安全框架中的核心问题
•     3.2.1 层次化建模
•     3.2.2 故障注入机制
•     3.2.3 故障模式及模型扩展
• 4 飞行引导系统的实例建模与安全性分析
•   4.1 GFC700实例系统概述
•   4.2 基于模型的系统安全性评估平台xSAP
•   4.3 飞行引导系统建模及模型扩展
•     4.3.1 NuSMV建模
•     4.3.2 故障注入与不变式的定义
•       4.3.2. 1 故障注入
•       4.3.2. 2 不变式
•     4.3.3 FEI故障模式
•   4.4 使用xSAP运行工具对飞行引导系统进行故障分析
•     4.4.1 模型扩展
•     4.4.2 验证系统性质
•     4.4.3 生成故障树
•     4.4.4 生成FMEA表
• 5 小结

文章来源

类型: 期刊论文

作者: 张维珺,胡军,李宛倩,陈朔,石梦烨,唐红英

关键词: 自动飞行控制系统,基于模型的安全性分析方法,模型扩展,故障树,失效模式与影响分析表

来源: 计算机科学与探索 2019年08期

年度: 2019

分类: 信息科技,工程科技Ⅱ辑

专业: 航空航天科学与工程

单位: 南京航空航天大学计算机科学与技术学院

基金: 国家重点基础研究发展计划(973计划)No.2014CB744903,南京航空航天大学研究生创新基地(实验室)开放基金No.kfjj20171611,中央高校基本科研业务费专项资金~~

分类号: V249.1

页码: 1295-1306

总页数: 12

文件大小: 1584K

下载量: 201