系统工程与电子技术 ›› 2023, Vol. 45 ›› Issue (5): 1553-1569.doi: 10.12305/j.issn.1001-506X.2023.05.33

• 可靠性 • 上一篇    

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

牛浩田1, 马存宝1,*, 韩佩2, 衣健民1   

  1. 1. 西北工业大学民航学院, 陕西 西安 710068
    2. 中国电子科技集团公司第20研究所, 陕西 西安 710068
  • 收稿日期:2022-08-25 出版日期:2023-04-21 发布日期:2023-04-28
  • 通讯作者: 马存宝
  • 作者简介:牛浩田(1989—), 男, 博士研究生, 主要研究方向为航电系统的任务安全性智能化分析与验证、民航规章知识图谱构建与应用
    马存宝(1964—), 男, 教授, 博士, 主要研究方向为飞机系统安全性分析、故障诊断、健康管理
    韩佩(1993—), 女, 工程师, 硕士, 主要研究方向为态势感知、实时系统建模与仿真
    衣健民(1992—), 男, 博士研究生, 主要研究方向为实时系统建模与仿真

Formal modeling and verification for mission safety of avionics system

Haotian NIU1, Cunbao MA1,*, Pei HAN2, Jianmin YI1   

  1. 1. School of Civil Aviation, Northwestern Polytechnical University, Xi'an 710068, China
    2. The 20th Institute, China Electronics Technology Corporation, Xi'an 710068, China
  • Received:2022-08-25 Online:2023-04-21 Published:2023-04-28
  • Contact: Cunbao MA

摘要:

针对航电系统任务安全性分析缺少仿真与验证手段问题, 提出了一种面向航电系统任务安全性的形式化建模与验证方法。首先, 基于时间自动机理论与民航规章建立标准运行条件下航电系统任务过程的形式化模型。随后, 将危险致因和安全约束分别以状态变迁的方式注入该模型, 建立航电系统任务安全性验证模型。最后, 通过遍历状态空间验证模型的活性、危险致因的可达性以及安全约束的充分性, 实现任务安全性分析结果的自动化验证。实验结果表明, 所提方法具有可行性和有效性, 能够为持续进行的航电系统任务安全性分析和设计提供模型基础, 确保分析结果的正确性和完整性。

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

Abstract:

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.

Key words: avionics system, mission safety, formal modeling, timed automata, simulation and verification

中图分类号: