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

Model-checking oriented unified modeling method based on NuSMV

作　　者：陈露 焦健[1] 魏钱锌 CHEN Lu;JIAO Jian;WEI Qianxin(School of Reliability and Systems Engineering,Beihang University,Beijing 100191,China)

机构地区：[1]北京航空航天大学可靠性与系统工程学院,北京100191

出　　处：《系统工程与电子技术》2018年第7期1654-1659,共6页Systems Engineering and Electronics

基　　金：国家重点基础研究发展计划(973计划)(2014CB744904)资助课题

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

关 键 词：故障 模型检查 安全性分析 基于模型的安全性分析 

分 类 号：X949[环境科学与工程—安全科学]