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

第一章 緒論

1.1  研究背景和意義

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

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

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

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

1.2.1  民航事故與不安全事件

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

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

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

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

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

2.1  故障樹分析技術(shù)

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

（1）  收集資料；

（2）  建立故障樹；

（3）  故障樹定性分析；

（4）  故障樹定量分析；

（5）  重要度分析；

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

2.2  故障樹建立

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

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

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

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

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

2.2.2  故障樹建立步驟

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

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

（2）確定頂事件。明確定義頂事件的判斷標(biāo)準(zhǔn)。 

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

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

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

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

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

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

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

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

4.1.2  語義驗(yàn)證 .............. 35

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

5.1  基于可擴(kuò)展標(biāo)記語言 XML 的模型表示 ..........53

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

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

5.1  基于可擴(kuò)展標(biāo)記語言 XML 的模型表示

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

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

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

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

參考文獻(xiàn)（略）