【摘要】 民航作為社會發(fā)展和國民經(jīng)濟的重要領域，是一項高投入、高技術和高風險的行業(yè)。民航業(yè)務系統(tǒng)安全水平是影響和制約民航業(yè)務發(fā)展的重要因素。隨著民航業(yè)務的發(fā)展，民航業(yè)務系統(tǒng)信息化也加速發(fā)展。民航業(yè)務系統(tǒng)規(guī)模越來越大，越來越復雜，在民航業(yè)務系統(tǒng)的研發(fā)過程中，迫切需要對系統(tǒng)進行安全性分析和驗證，但目前相關方面的研究和實踐工作較薄弱。本文正是針對目前民航業(yè)務系統(tǒng)安全性研究的不足和現(xiàn)實需求，試圖研究一種可行的安全性分析方法和相關的驗證算法，對民航業(yè)務系統(tǒng)進行安全性分析和驗證。本文主要研究內(nèi)容如下：(1)引入故障樹分析技術進行民航業(yè)務系統(tǒng)模型的安全性分析。針對民航業(yè)務系統(tǒng)的簽派系統(tǒng)中典型事故進行總結(jié)，根據(jù)故障樹底事件找出業(yè)務系統(tǒng)不安全的底層原因并對其進行定性分析，確定安全性需求。(2)提出基于有向圖的民航業(yè)務系統(tǒng)模型ABPD。該模型將數(shù)據(jù)間的依賴關系引入到傳統(tǒng)業(yè)務流程模型中，不但能夠在順序流中表達任務之間的邏輯關系，也能夠描述數(shù)據(jù)間邏輯關系。(3)分析民航業(yè)務系統(tǒng)的安全性并設計安全性驗證方法。根據(jù)民航安全性需求，總結(jié)安全性約束條件，提出6類安全性，進一步設計出基于ABPD模型的圖搜索的民航業(yè)務系統(tǒng)安全性驗證算法。(4)安全性驗證方法實現(xiàn)。引入XML可擴展標記語言對ABPD模型進行描述，分析模型中節(jié)點的關系，給出模型的數(shù)據(jù)結(jié)構(gòu)，實現(xiàn)民航業(yè)務系統(tǒng)安全性驗證算法，最后使用MFC編寫驗證程序，形成一個驗證工具原型。系統(tǒng)運行和測試結(jié)果表明，本文提出的方法可以對相關安全性質(zhì)進行有效驗證。 

第一章 緒論

1.1  研究背景和意義

改革開放以來，隨著國民經(jīng)濟飛速發(fā)展和民航市場需求的快速增長，我國民航事業(yè)取得了蓬勃發(fā)展，國內(nèi)航線不斷擴充，航班密度持續(xù)增大，2012 年 1 月至 12 月民航旅客運輸量累計為 3.19 億人次，同比增長 9.2%。目前，我國已是僅次于美國的全球第二大民航市場。據(jù)空中客車公司預測，20 年后我國國內(nèi)航空客運周轉(zhuǎn)量將超過美國，成為全球航空客運周轉(zhuǎn)量第一的國內(nèi)航空客運市場。

隨著規(guī)模的擴大，為了順應市場規(guī)律，民航企業(yè)對業(yè)務系統(tǒng)信息化建設也逐步重視，其投入不斷加大，每年在固定資產(chǎn)投資中安排了一定比例的資金用于業(yè)務系統(tǒng)建設，效果顯著。如各大航空公司紛紛改革經(jīng)營模式和業(yè)務流程，成立運行控制中心，推廣使用航班運行控制（Flight Operations  Control，F(xiàn)OC）業(yè)務系統(tǒng)。FOC 是航空公司運行的決策中心，是保證飛行安全的系統(tǒng)，保障航空公司的安全、正常、舒適和經(jīng)濟效益。FOC 系統(tǒng)實現(xiàn)了航班計劃、航班動態(tài)、飛機計劃、機組信息、飛行數(shù)據(jù)、航行情報、航路數(shù)據(jù)等方面的信息共享。

我國民航業(yè)務系統(tǒng)建設極大地推動了民航業(yè)的蓬勃發(fā)展，然而在促進民航業(yè)進步的同時，也存在一些不容忽視的問題。首先，民航業(yè)務系統(tǒng)十分復雜，設計過程中易隱含錯誤。由圖 1.1可見，  FOC系統(tǒng)覆蓋從航班計劃到飛行執(zhí)行完畢的整個航班生產(chǎn)過程，涉及到航班計劃管理、飛機調(diào)度、機組管理、商務調(diào)度、航行情報、飛行簽派管理的全部生產(chǎn)部門。FOC 系統(tǒng)實現(xiàn)時可劃分為 10 至 20 多個主要的功能系統(tǒng)，而與其他系統(tǒng)的接口又有 10 至 20 個。如果再考慮各個功能系統(tǒng)的流程等，F(xiàn)OC 系統(tǒng)將更加復雜。復雜的民航業(yè)務系統(tǒng)設計過程中難免產(chǎn)生錯誤。并且，系統(tǒng)越復雜，存在的錯誤也越多，隱蔽性也越大。

1.2  國內(nèi)外研究現(xiàn)狀及存在問題

1.2.1  民航事故與不安全事件

隨著民航運輸量的快速增長，我國民航的新的發(fā)展階段已經(jīng)來臨。根據(jù)波音飛機公司的年度預測報過，在未來的 20 年內(nèi)，中國民航旅客運輸量的年增長率約為 7.4%，貨物運輸量的年增長率約為 9%。到 2023 年，我國飛機數(shù)量將增長至現(xiàn)今的 3 倍。但是，根據(jù)我國目前的航空業(yè)發(fā)展速度和近十年來的航空飛行重大事故率計算，在 2015 年和 2020 年，我國民航運輸中將分別發(fā)生重大飛行事故 3.1 次和 4.6 次。由于民航運輸相比其他運輸業(yè)具有更高的安全期望，顯然上述事故率是無法被國家和人民接受的。

近年來從業(yè)人員不斷改善安全監(jiān)管體系，統(tǒng)一和完善了民航運行有關的安全法規(guī)和標準，我國的民航安全得到的極大的改善，但是民航不安全事件仍然時有發(fā)生。圖 1.2 是我國民航近十年來的二等和重大飛行事故柱狀圖，圖 1.3是 2011 年度事故征候分析圖。

由圖 1.2、圖 1.3 可見，近年來民航中事故/與不安全事件屢有發(fā)生，其中系統(tǒng)失效占有很大比例。我國的民航安全雖然高于國際安全水平，但與發(fā)達國家仍有差距，仍有潛力可挖掘，安全水平仍有提高空間。本文針對民航業(yè)務系統(tǒng)模型討論民航業(yè)務系統(tǒng)研究中的共性問題——安全性問題及其驗證方法。

第二章 基于故障樹的民航業(yè)務系統(tǒng)安全性分析

近年來，民航事故/不安全事屢有發(fā)生，原因復雜多樣。如何針對民航業(yè)務特殊性定義安全性對安全性驗證工作十分重要。按照民航業(yè)務現(xiàn)有安全水平和運輸量增長速度，至 2015 年將會發(fā)生多起飛機失事。為了解決這個問題，專家提出零事故目標和安全第一原則。事故發(fā)生的可能性總是存在，為了預防事故的發(fā)生，需要仔細研究事故根源，確定安全性需求，防止發(fā)生更嚴重的事故。本章引入故障樹分析技術，很好地分析事故發(fā)生的直接原因和間接原因。本章對近年來典型民航事故/不安全事件分析，找出引起民航不安全事件的底層故障事件，并對故障樹定性分析，進一步確定故障成因，提取出安全性需求，從而有目標地對民航業(yè)務系統(tǒng)進行安全性驗證。

2.1  故障樹分析技術

故障樹分析技術由美國貝爾實驗室開發(fā)，最初用于導彈發(fā)生系統(tǒng)的質(zhì)量評估。美國航空航天局與國防部于上世紀六十年代初發(fā)展了故障樹分析技術（Faulty Tree Analysis）。由于故障樹分析技術的直觀明了，靈活多用且邏輯性強，，在隨后的幾十年來，故障樹技術在民航、載人航天、導彈系統(tǒng)、大型核電站事故分析中得到大范圍推廣和應用。 故障樹分析的一般步驟如下圖 2.1 所示：

（1）  收集資料；

（2）  建立故障樹；

（3）  故障樹定性分析；

（4）  故障樹定量分析；

（5）  重要度分析；

（6）  分析結(jié)論。

2.2  故障樹建立

故障樹建立是故障樹分析的核心步驟。能否層次分明，建立正確的故障樹，將直接影響故障樹分析結(jié)果的準確性。

為龐大復雜的民航業(yè)務系統(tǒng)建立專門的故障樹需要大量的前期準備，需要熟悉掌握民航業(yè)務系統(tǒng)的結(jié)構(gòu)和功能，詳細分析基本單元事件之間的聯(lián)系。通過建立故障樹，可以有效定位民航業(yè)務系統(tǒng)潛在的故障因素，獲取安全性需求，并對系統(tǒng)進行改進和完善。

2.2.1  故障樹構(gòu)建方式 故障樹的建立方式主要有手動建樹和計算機輔助建樹兩種。

手動建樹又稱演繹法。手動建樹采用非常普遍，可以快速便利的定位全部的故障模式和原因。建樹人員根據(jù)系統(tǒng)的故障因果關系，從系統(tǒng)的頂事件自上而下地演繹出頂事件的直接原因。根據(jù)頂事件->邏輯門->中間事件->邏輯門->底事件的順序推導，直到所有底事件推理完為止。

計算機輔助建樹又稱合成法。主要通過匯總系統(tǒng)的基本單元的失效函數(shù)，根據(jù)一定的邊界條件，從系統(tǒng)的頂事件自頂而下采用計算機程序按照規(guī)定的約束自動生成系統(tǒng)故障樹。目前多采用有向圖法、小故障樹合成法、節(jié)點關系圖法和決策表法進行輔助建樹。但是由于缺乏有效的方式進行智能判斷區(qū)分出薄弱環(huán)節(jié)，并且專家“故障診斷”尚難以用計算機描述，因此國內(nèi)的計算機輔助建立故障樹還在探索階段未大規(guī)模應用。

2.2.2  故障樹建立步驟

由于計算機輔助建樹技術尚未成熟，本文采用手動演繹法建立民航故障樹。建樹具體步驟如下：

（1）詳細分析民航系統(tǒng)的結(jié)構(gòu)與工作原理，收集民航系統(tǒng)的設計文檔、運行資料、工作流程等相關技術數(shù)據(jù)。

（2）確定頂事件。明確定義頂事件的判斷標準。 

（3）找出引起頂事件發(fā)生的直接原因。選取適當?shù)倪壿嬮T，將頂事件作為輸出事件，直接原因事件作為輸入事件從而明確事件之間的因果關系。 

（4）逐層向下演繹分析，直到所有的輸入事件都不必或者不能再進行分解為止，此時的輸入事件為底事件。   根據(jù)以上步驟可以構(gòu)建出系統(tǒng)的故障樹。本章將以民航飛行控制簽派系統(tǒng)為例構(gòu)建故障樹進行分析。

 第三章  民航業(yè)務系統(tǒng)的 ABPD 模型 ...... 26

3.1  業(yè)務流程模型元素 ............ 26

3.1.1  業(yè)務流程基本視圖 ......26

第四章  民航業(yè)務系統(tǒng)模型的安全性驗證算法設計 ...............34

4.1  業(yè)務流程模型驗證方式 ............ 34

4.1.1  結(jié)構(gòu)驗證 .................. 34

4.1.2  語義驗證 .............. 35

第五章  民航業(yè)務系統(tǒng)的安全性驗證的實現(xiàn) ................ 53

5.1  基于可擴展標記語言 XML 的模型表示 ..........53

第五章 民航業(yè)務系統(tǒng)的安全性驗證的實現(xiàn)

本文在上一章定義了民航業(yè)務系統(tǒng)的安全性，約束了什么不應該發(fā)生；并結(jié)合第三章的ABPD 模型設計了 DTM 矩陣，提出民航業(yè)務系統(tǒng)安全性驗證算法。為了實現(xiàn)該驗證算法，本章將引入 XML 可擴展標記語言描述模型設計實現(xiàn)一個驗證工具原型，支持給定民航業(yè)務系統(tǒng)模型的安全性驗證，實現(xiàn)包括原始模型信息輸入，求解網(wǎng)關對應關系、并行節(jié)點以及 DTM矩陣，最后驗證模型安全性輸出異常。本章以第四章的安全性為基礎，以民航業(yè)務流程模型為輸入，以驗證結(jié)果為輸出，將所有的驗證模塊進行整合并協(xié)同工作。

5.1  基于可擴展標記語言 XML 的模型表示

民航業(yè)務系統(tǒng)安全性驗證需要有一個優(yōu)良的建模方案，由于它處理大量的非數(shù)字的信息，在模型相關信息輸入時需要有一個很好的中間表示手段。本節(jié)在分析 ABPD 模型的數(shù)據(jù)結(jié)構(gòu)的基礎上引入 XML 可擴展標記語言以定義模型，增強了模型的可操作性和可擴展性�；�于 XML的模型具有規(guī)范的格式，很好的擴展性和重用性，并且易于管理和使用。

第六章 總結(jié)與展望

民航業(yè)務系統(tǒng)的安全性分析與驗證是十分富有現(xiàn)實意義的研究課題。為了保證民航業(yè)務系統(tǒng)的安全性，必須對民航業(yè)務模型進行安全性分析、形式化建模與驗證，以避免在業(yè)務系統(tǒng)執(zhí)行中任務出現(xiàn)死鎖、同步缺失、任務前提數(shù)據(jù)異常、任務依賴數(shù)據(jù)異常等問題。因此，進行民航業(yè)務系統(tǒng)的安全性分析與驗證的研究對于實施新的或改進已有的民航業(yè)務系統(tǒng)具有積極的意義。近年來很多專家對其進行了深入的研究和探討，并提出了一些可行的方法。但就目前的文獻而言，針對民航業(yè)務系統(tǒng)中數(shù)據(jù)模型與業(yè)務流程模型相結(jié)合的安全性驗證研究領域還局限于理論研究階段。本文重點分析民航業(yè)務系統(tǒng)的安全性，研究并實現(xiàn)數(shù)據(jù)模型與業(yè)務流程模型相結(jié)合的民航業(yè)務系統(tǒng)建模與安全性驗證方法。

本文首先詳細介紹論文選題的背景與意義，隨后綜述民航業(yè)務系統(tǒng)的安全性分析與驗證領域的研究進展。文章從民航系統(tǒng)和業(yè)務流程模型的安全性研究現(xiàn)狀出發(fā)，使用故障樹分析技術對民航簽派系統(tǒng)中的故障事件進行分析，發(fā)現(xiàn)民航業(yè)務系統(tǒng)中業(yè)務流程模型設計時可能包含結(jié)構(gòu)沖突，也可能隱含大量語義沖突，為民航安全埋下隱患。其次，為了驗證民航業(yè)務系統(tǒng)的安全性，即“壞的事情不發(fā)生”，結(jié)合數(shù)據(jù)模型對民航業(yè)務流程模型進行有效的形式化建模，本文在傳統(tǒng)的業(yè)務流程中引入數(shù)據(jù)間的邏輯關系建立基于有向圖的 ABPD 模型。再次，根據(jù)模型中任務之間、任務與數(shù)據(jù)之間、數(shù)據(jù)之間的交互提出新的模型異常，從流程的結(jié)構(gòu)和語義層次使用謂詞結(jié)構(gòu)定義民航業(yè)務流程模型中的安全性。為減少后期驗證的復雜度提出并行任務集合對ABPD 模型中順行流節(jié)點進行并行分析，減少搜索量；再基于并行集合提出 DTM 矩陣分析數(shù)據(jù)對象在各任務執(zhí)行時的存在狀態(tài)，最后使用圖搜索方法對 ABPD 模型進行安全性驗證。實驗結(jié)果表明，本文提出的基于 ABPD 模型的民航業(yè)務系統(tǒng)安全性驗證方法可以很好地驗證業(yè)務系統(tǒng)中潛在的業(yè)務流程模型與數(shù)據(jù)模型的不一致性，并在存在大量并行結(jié)構(gòu)的民航業(yè)務系統(tǒng)中有效減少搜索量，縮短驗證時間，對民航業(yè)務系統(tǒng)安全性驗證有實際的意義。

參考文獻（略）