面向航电系统任务安全性的形式化建模与验证  

Formal modeling and verification for mission safety of avionics system

作　　者：牛浩田 马存宝[1] 韩佩 衣健民 NIU Haotian;MA Cunbao;HAN Pei;YI Jianmin(School of Civil Aviation,Northwestern Polytechnical University,Xi’an 710068,China;The 20th Institute,China Electronics Technology Corporation,Xi’an 710068,China)

机构地区：[1]西北工业大学民航学院,陕西西安710068 [2]中国电子科技集团公司第20研究所,陕西西安710068

出　　处：《系统工程与电子技术》2023年第5期1553-1569,共17页Systems Engineering and Electronics

基　　金：国家自然科学基金面上项目(12172290,61873203);国家自然科学基金青年科学基金(51805434);国家重点基础研究发展项目(973计划)(2014CB744902)资助课题。

摘　　要：针对航电系统任务安全性分析缺少仿真与验证手段问题,提出了一种面向航电系统任务安全性的形式化建模与验证方法。首先,基于时间自动机理论与民航规章建立标准运行条件下航电系统任务过程的形式化模型。随后,将危险致因和安全约束分别以状态变迁的方式注入该模型,建立航电系统任务安全性验证模型。最后,通过遍历状态空间验证模型的活性、危险致因的可达性以及安全约束的充分性,实现任务安全性分析结果的自动化验证。实验结果表明,所提方法具有可行性和有效性,能够为持续进行的航电系统任务安全性分析和设计提供模型基础,确保分析结果的正确性和完整性。In view of lacking simulation and verification means for mission safety analysis of avionics system,a formal modeling and verification method for mission safety of avionics system is proposed.A formal model of avionics system’mission process under standard operating conditions is formed based on timed automata theory and aviation regulations firstly.Then,hazard causes and safe constraints are integrated into the model as state transitions to construct verification model of mission safety for avionics system,respectively.Finally,by traversing the state space to verify the activity of the model,the accessibility of the hazard causes and the adequacy of the safe constraints,the automatic verification of the task security analysis results is realized.Experimental results show that the proposed method is feasible and effective.The method can provide a model basis for the ongoing process of mission safety analysis and design for avionics system,as well as ensure the correctness and integrity of the analysis results.

关 键 词：航电系统 任务安全性 形式化建模 时间自动机 仿真验证 

分 类 号：V267[航空宇航科学与技术—航空宇航制造工程]