西安电子科技大学学报 ›› 2019, Vol. 46 ›› Issue (3): 66-73.doi: 10.19665/j.issn1001-2400.2019.03.011

• • 上一篇    下一篇

一种航空电子系统安全性需求验证方法

丁明1,2,张书玲1,张琛3,张军2   

  1. 1. 西北大学 信息科学与技术学院,陕西 西安 710127
    2. 西安航空计算技术研究所,陕西 西安 710119
    3. 西安电子科技大学 计算机科学与技术学院,陕西 西安 710071
  • 收稿日期:2019-01-06 出版日期:2019-06-20 发布日期:2019-06-19
  • 作者简介:丁 明 (1982-),男,高级工程师,西北大学博士研究生,E-mail: dingmingdm@126.com.
  • 基金资助:
    国家自然科学基金(61502365);陕西省重点研发计划一般项目(2019GY-042)

Method for the verification of safety requirements of avionics systems

DING Ming1,2,ZHANG Shuling1,ZHANG Chen3,Zhang Jun2   

  1. 1. School of Information Science and Technology, Northwest University, Xi'an, 710127, China
    2. Xi'an Aeronautics Computing Technique Research Institute, AVIC, Xi'an, 710119, China
    3. School of Computer Science and Technology, Xidian University, Xi'an, 710071, China
  • Received:2019-01-06 Online:2019-06-20 Published:2019-06-19

摘要:

针对航空电子系统安全性评估过程中正确性难以保证的问题,在研究系统安全性模型的基础上,提出了一种基于模型的系统安全性需求描述和验证方法。该方法首先针对系统功能需求、安全性目标和失效状态建立危害用例,提取安全性需求;然后,采用带功能失效的状态机图描述包含安全性需求的系统功能模型,并使用安全扩展层次自动机作为中间状态,通过转换算法实现系统功能模型的形式化描述;最后,通过模型检测实现安全性需求的正确性验证。实例分析表明,该方法能够验证设计的系统功能是否满足安全性属性,提升安全性评估的准确性和效率。

关键词: 航空电子系统, 安全性, 形式化方法, 模型检测

Abstract:

To ensure the correctness of avionics systems safety assessment, a model-based system safety requirements description and verification approach is proposed. First, hazard use cases are established and safety requirements are captured according to the system functional requirements, safety objectives and failure states. Second, the state machine diagrams with functional failure are used to describe the system functional model including safety requirements. The safety extended hierarchical automata are used as the intermediate models, and the formal description of the system functional model is realized by the transformation algorithm. Finally, the correctness of safety requirements is verified by model checking. Case studies are presented to show that this method can verify whether the designed system's functions meet the safety attributes and improve the accuracy and efficiency of safety assessment.

Key words: avionics systems, safety, formal methods, model checking

中图分类号: 

  • TP311