面向模型检查的NuSMV统一建模方法

• 作者: 焦健 陈露 魏钱锌
• 来源期刊: 系统工程与电子技术
• 学科: 工学
• 关键词: 故障 模型检查 安全性分析 基于模型的安全性分析
• 年，卷（期）: 2018,（7）
• 所属期刊栏目: 可靠性
• 页码范围: 1654-1659
• 页数: 6页
• 分类号: X949
• 字数: 5672字
• 语种: 中文
• DOI: 10.3969/j.issn.1001-506X.2018.07.34

摘要

以形式化建模和利用模型检查进行自动化分析验证为核心的基于模型的安全性分析(model based safety analysis ,MBSA )技术能够提高工作效率和分析结果的客观性,已在复杂大型装备系统的安全性工作中得到广泛重视与应用.现有的 MBSA框架下的建模过程较为复杂,且通常需要模型转换,易造成模型信息的损失,影响安全性分析结果的准确性和全面性.面向模型检查,提出了基于符号语言构建统一系统模型的方法,研究了形式化语言元素与系统功能、结构和故障模式之间的分配与映射关系,利用时态逻辑公式规范了系统安全性要求的定义.最后,以飞控系统的前主桨舵机为例进行了案例应用,验证建模方法的有效性和适用性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	焦健	北京航空航天大学可靠性与系统工程学院	24	97	5.0	9.0
2	陈露	北京航空航天大学可靠性与系统工程学院	1	2	1.0	1.0
3	魏钱锌	北京航空航天大学可靠性与系统工程学院	1	2	1.0	1.0