计算机与现代化

• 应用与开发 • 上一篇    下一篇

民航业务系统的安全性分析与验证

  

  1. 南京航空航天大学计算机科学与技术学院,江苏南京210016
  • 收稿日期:2014-07-16 出版日期:2014-11-03 发布日期:2014-11-05
  • 作者简介:邢逆舟(1990-),男,安徽宣城人,南京航空航天大学计算机科学与技术学院硕士研究生,研究方向:航空电子,〖JP2〗软件工程,分布式计算; 王立松(1969-),男,江苏南京人,副教授,博士,研究方向:航空电子,软件工程,分布式计算,操作系统。
  • 基金资助:
    国家重点基础研究发展计划项目(2014CB744900)

Safety Analysis and Verification on Civil Aviation Business System

  1. College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 210016, China
  • Received:2014-07-16 Online:2014-11-03 Published:2014-11-05

摘要: 民航业务系统正确处理民航业务逻辑是民航企业运行的必要条件,因此民航业务系统的安全性十分重要,形式化验证方法是保障系统安全性的重要技术手段。本文结合故障树分析技术提取民航业务逻辑的安全性验证需求,并用新〖JP2〗提出的ABPD业务流程模型为民航业务系统建模,进一步分析并定义出6种安全性性质。最后,采用图搜索方法对ABPD〖JP〗模型进行安全性验证并给出具体算法实现。实验结果表明了算法和程序的有效性。

关键词: 民航业务系统, 故障树分析技术, ABPD模型, 安全性验证, 模型验证

Abstract: The safety of the civil aviation business system is very important because it is a necessary condition for civil aviation enterprise to run. Formal verification method is an important approach to insuring system safety. In this paper, firstly, the fault tree analysis technology is introduced to analyze the safety requirements and the new ABPD modeling language is promoted. Secondly, six kinds of safety properties are defined through analyzing the model. Thirdly, safety verification is achieved through graph search algorithm and the concrete implementation of the algorithm is provided. Lastly, the experiment results explain the completed verification process and the validity of the method.

Key words: civil aviation business system, fault tree analysis technology, ABPD modeling, safety verification, model verification

中图分类号: