系统工程与电子技术 ›› 2018, Vol. 40 ›› Issue (7): 1654-1659.doi: 10.3969/j.issn.1001-506X.2018.07.34

• 可靠性 • 上一篇    下一篇

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

陈露, 焦健, 魏钱锌   

  1. 北京航空航天大学可靠性与系统工程学院,北京 100191
  • 出版日期:2018-06-26 发布日期:2018-06-28

Model-checking oriented unified modeling method based on NuSMV

CHEN Lu, JIAO Jian, WEI Qianxin   

  1. School of Reliability and Systems Engineering, Beihang University, Beijing 100191, China
  • Online:2018-06-26 Published:2018-06-28

摘要:

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

Abstract:

Formal modeling and automated analysis and verification based on model checking are the core of the model based safety analysis (MBSA) technology. MBSA has gained wide attention and application in the safety work of large complex equipment system, for the reason that it improves the work efficiency and objectivity of the analysis results. The existing modeling process under the MBSA framework is relatively complex, and often needs model transformation, which results in information loss easily and affects the accuracy and completeness of safety analysis results. A model-checking oriented unified system modeling method using symbolic language is proposed, including the mapping relationships between the formal language elements and system functions, architecture and fault modes as well as the normalized definitions of system safety requirements using temporal logic formulas. Finally, a case study about the actuator system of the flight control system is provided to validate the availability and applicability of the modeling method.