民航业务系统的安全性分析与验证方法研究

【摘要】 民航作为社会发展和国民经济的重要领域，是一项高投入、高技术和高风险的行业。民航业务系统安全水平是影响和制约民航业务发展的重要因素。随着民航业务的发展，民航业务系统信息化也加速发展。民航业务系统规模越来越大，越来越复杂，在民航业务系统的研发过程中，迫切需要对系统进行安全性分析和验证，但目前相关方面的研究和实践工作较薄弱。本文正是针对目前民航业务系统安全性研究的不足和现实需求，试图研究一种可行的安全性分析方法和相关的验证算法，对民航业务系统进行安全性分析和验证。本文主要研究内容如下：(1)引入故障树分析技术进行民航业务系统模型的安全性分析。针对民航业务系统的签派系统中典型事故进行总结，根据故障树底事件找出业务系统不安全的底层原因并对其进行定性分析，确定安全性需求。(2)提出基于有向图的民航业务系统模型ABPD。该模型将数据间的依赖关系引入到传统业务流程模型中，不但能够在顺序流中表达任务之间的逻辑关系，也能够描述数据间逻辑关系。(3)分析民航业务系统的安全性并设计安全性验证方法。根据民航安全性需求，总结安全性约束条件，提出6类安全性，进一步设计出基于ABPD模型的图搜索的民航业务系统安全性验证算法。(4)安全性验证方法实现。引入XML可扩展标记语言对ABPD模型进行描述，分析模型中节点的关系，给出模型的数据结构，实现民航业务系统安全性验证算法，最后使用MFC编写验证程序，形成一个验证工具原型。系统运行和测试结果表明，本文提出的方法可以对相关安全性质进行有效验证。 

第一章 绪论

1.1  研究背景和意义

改革开放以来，随着国民经济飞速发展和民航市场需求的快速增长，我国民航事业取得了蓬勃发展，国内航线不断扩充，航班密度持续增大，2012 年 1 月至 12 月民航旅客运输量累计为 3.19 亿人次，同比增长 9.2%。目前，我国已是仅次于美国的全球第二大民航市场。据空中客车公司预测，20 年后我国国内航空客运周转量将超过美国，成为全球航空客运周转量第一的国内航空客运市场。

随着规模的扩大，为了顺应市场规律，民航企业对业务系统信息化建设也逐步重视，其投入不断加大，每年在固定资产投资中安排了一定比例的资金用于业务系统建设，效果显著。如各大航空公司纷纷改革经营模式和业务流程，成立运行控制中心，推广使用航班运行控制（Flight Operations  Control，FOC）业务系统。FOC 是航空公司运行的决策中心，是保证飞行安全的系统，保障航空公司的安全、正常、舒适和经济效益。FOC 系统实现了航班计划、航班动态、飞机计划、机组信息、飞行数据、航行情报、航路数据等方面的信息共享。

我国民航业务系统建设极大地推动了民航业的蓬勃发展，然而在促进民航业进步的同时，也存在一些不容忽视的问题。首先，民航业务系统十分复杂，设计过程中易隐含错误。由图 1.1可见，  FOC系统覆盖从航班计划到飞行执行完毕的整个航班生产过程，涉及到航班计划管理、飞机调度、机组管理、商务调度、航行情报、飞行签派管理的全部生产部门。FOC 系统实现时可划分为 10 至 20 多个主要的功能系统，而与其他系统的接口又有 10 至 20 个。如果再考虑各个功能系统的流程等，FOC 系统将更加复杂。复杂的民航业务系统设计过程中难免产生错误。并且，系统越复杂，存在的错误也越多，隐蔽性也越大。

1.2  国内外研究现状及存在问题

1.2.1  民航事故与不安全事件

随着民航运输量的快速增长，我国民航的新的发展阶段已经来临。根据波音飞机公司的年度预测报过，在未来的 20 年内，中国民航旅客运输量的年增长率约为 7.4%，货物运输量的年增长率约为 9%。到 2023 年，我国飞机数量将增长至现今的 3 倍。但是，根据我国目前的航空业发展速度和近十年来的航空飞行重大事故率计算，在 2015 年和 2020 年，我国民航运输中将分别发生重大飞行事故 3.1 次和 4.6 次。由于民航运输相比其他运输业具有更高的安全期望，显然上述事故率是无法被国家和人民接受的。

近年来从业人员不断改善安全监管体系，统一和完善了民航运行有关的安全法规和标准，我国的民航安全得到的极大的改善，但是民航不安全事件仍然时有发生。图 1.2 是我国民航近十年来的二等和重大飞行事故柱状图，图 1.3是 2011 年度事故征候分析图。

由图 1.2、图 1.3 可见，近年来民航中事故/与不安全事件屡有发生，其中系统失效占有很大比例。我国的民航安全虽然高于国际安全水平，但与发达国家仍有差距，仍有潜力可挖掘，安全水平仍有提高空间。本文针对民航业务系统模型讨论民航业务系统研究中的共性问题——安全性问题及其验证方法。

第二章 基于故障树的民航业务系统安全性分析

近年来，民航事故/不安全事屡有发生，原因复杂多样。如何针对民航业务特殊性定义安全性对安全性验证工作十分重要。按照民航业务现有安全水平和运输量增长速度，至 2015 年将会发生多起飞机失事。为了解决这个问题，专家提出零事故目标和安全第一原则。事故发生的可能性总是存在，为了预防事故的发生，需要仔细研究事故根源，确定安全性需求，防止发生更严重的事故。本章引入故障树分析技术，很好地分析事故发生的直接原因和间接原因。本章对近年来典型民航事故/不安全事件分析，找出引起民航不安全事件的底层故障事件，并对故障树定性分析，进一步确定故障成因，提取出安全性需求，从而有目标地对民航业务系统进行安全性验证。

2.1  故障树分析技术

故障树分析技术由美国贝尔实验室开发，最初用于导弹发生系统的质量评估。美国航空航天局与国防部于上世纪六十年代初发展了故障树分析技术（Faulty Tree Analysis）。由于故障树分析技术的直观明了，灵活多用且逻辑性强，，在随后的几十年来，故障树技术在民航、载人航天、导弹系统、大型核电站事故分析中得到大范围推广和应用。 故障树分析的一般步骤如下图 2.1 所示：

（1）  收集资料；

（2）  建立故障树；

（3）  故障树定性分析；

（4）  故障树定量分析；

（5）  重要度分析；

（6）  分析结论。

2.2  故障树建立

故障树建立是故障树分析的核心步骤。能否层次分明，建立正确的故障树，将直接影响故障树分析结果的准确性。

为庞大复杂的民航业务系统建立专门的故障树需要大量的前期准备，需要熟悉掌握民航业务系统的结构和功能，详细分析基本单元事件之间的联系。通过建立故障树，可以有效定位民航业务系统潜在的故障因素，获取安全性需求，并对系统进行改进和完善。

2.2.1  故障树构建方式 故障树的建立方式主要有手动建树和计算机辅助建树两种。

手动建树又称演绎法。手动建树采用非常普遍，可以快速便利的定位全部的故障模式和原因。建树人员根据系统的故障因果关系，从系统的顶事件自上而下地演绎出顶事件的直接原因。根据顶事件->逻辑门->中间事件->逻辑门->底事件的顺序推导，直到所有底事件推理完为止。

计算机辅助建树又称合成法。主要通过汇总系统的基本单元的失效函数，根据一定的边界条件，从系统的顶事件自顶而下采用计算机程序按照规定的约束自动生成系统故障树。目前多采用有向图法、小故障树合成法、节点关系图法和决策表法进行辅助建树。但是由于缺乏有效的方式进行智能判断区分出薄弱环节，并且专家“故障诊断”尚难以用计算机描述，因此国内的计算机辅助建立故障树还在探索阶段未大规模应用。

2.2.2  故障树建立步骤

由于计算机辅助建树技术尚未成熟，本文采用手动演绎法建立民航故障树。建树具体步骤如下：

（1）详细分析民航系统的结构与工作原理，收集民航系统的设计文档、运行资料、工作流程等相关技术数据。

（2）确定顶事件。明确定义顶事件的判断标准。 

（3）找出引起顶事件发生的直接原因。选取适当的逻辑门，将顶事件作为输出事件，直接原因事件作为输入事件从而明确事件之间的因果关系。 

（4）逐层向下演绎分析，直到所有的输入事件都不必或者不能再进行分解为止，此时的输入事件为底事件。   根据以上步骤可以构建出系统的故障树。本章将以民航飞行控制签派系统为例构建故障树进行分析。

 第三章  民航业务系统的 ABPD 模型 ...... 26

3.1  业务流程模型元素 ............ 26

3.1.1  业务流程基本视图 ......26

第四章  民航业务系统模型的安全性验证算法设计 ...............34

4.1  业务流程模型验证方式 ............ 34

4.1.1  结构验证 .................. 34

4.1.2  语义验证 .............. 35

第五章  民航业务系统的安全性验证的实现 ................ 53

5.1  基于可扩展标记语言 XML 的模型表示 ..........53

第五章 民航业务系统的安全性验证的实现

本文在上一章定义了民航业务系统的安全性，约束了什么不应该发生；并结合第三章的ABPD 模型设计了 DTM 矩阵，提出民航业务系统安全性验证算法。为了实现该验证算法，本章将引入 XML 可扩展标记语言描述模型设计实现一个验证工具原型，支持给定民航业务系统模型的安全性验证，实现包括原始模型信息输入，求解网关对应关系、并行节点以及 DTM矩阵，最后验证模型安全性输出异常。本章以第四章的安全性为基础，以民航业务流程模型为输入，以验证结果为输出，将所有的验证模块进行整合并协同工作。

5.1  基于可扩展标记语言 XML 的模型表示

民航业务系统安全性验证需要有一个优良的建模方案，由于它处理大量的非数字的信息，在模型相关信息输入时需要有一个很好的中间表示手段。本节在分析 ABPD 模型的数据结构的基础上引入 XML 可扩展标记语言以定义模型，增强了模型的可操作性和可扩展性。基于 XML的模型具有规范的格式，很好的扩展性和重用性，并且易于管理和使用。

第六章 总结与展望

民航业务系统的安全性分析与验证是十分富有现实意义的研究课题。为了保证民航业务系统的安全性，必须对民航业务模型进行安全性分析、形式化建模与验证，以避免在业务系统执行中任务出现死锁、同步缺失、任务前提数据异常、任务依赖数据异常等问题。因此，进行民航业务系统的安全性分析与验证的研究对于实施新的或改进已有的民航业务系统具有积极的意义。近年来很多专家对其进行了深入的研究和探讨，并提出了一些可行的方法。但就目前的文献而言，针对民航业务系统中数据模型与业务流程模型相结合的安全性验证研究领域还局限于理论研究阶段。本文重点分析民航业务系统的安全性，研究并实现数据模型与业务流程模型相结合的民航业务系统建模与安全性验证方法。

本文首先详细介绍论文选题的背景与意义，随后综述民航业务系统的安全性分析与验证领域的研究进展。文章从民航系统和业务流程模型的安全性研究现状出发，使用故障树分析技术对民航签派系统中的故障事件进行分析，发现民航业务系统中业务流程模型设计时可能包含结构冲突，也可能隐含大量语义冲突，为民航安全埋下隐患。其次，为了验证民航业务系统的安全性，即“坏的事情不发生”，结合数据模型对民航业务流程模型进行有效的形式化建模，本文在传统的业务流程中引入数据间的逻辑关系建立基于有向图的 ABPD 模型。再次，根据模型中任务之间、任务与数据之间、数据之间的交互提出新的模型异常，从流程的结构和语义层次使用谓词结构定义民航业务流程模型中的安全性。为减少后期验证的复杂度提出并行任务集合对ABPD 模型中顺行流节点进行并行分析，减少搜索量；再基于并行集合提出 DTM 矩阵分析数据对象在各任务执行时的存在状态，最后使用图搜索方法对 ABPD 模型进行安全性验证。实验结果表明，本文提出的基于 ABPD 模型的民航业务系统安全性验证方法可以很好地验证业务系统中潜在的业务流程模型与数据模型的不一致性，并在存在大量并行结构的民航业务系统中有效减少搜索量，缩短验证时间，对民航业务系统安全性验证有实际的意义。

参考文献（略）