發(fā)布時間：2018-08-28 11:57

【摘要】：管制員響應(yīng)執(zhí)行是空中交通管制的重要環(huán)節(jié),也是民航空管運行中易引發(fā)不安全事件的關(guān)鍵過程。為了對涉及管制員響應(yīng)執(zhí)行過程的不安全事件進行深入分析,提高事件分析的規(guī)范性和自動化程度,避免過分利用自然語言描述的缺點,提出了基于時態(tài)邏輯的形式化推理方法。首先,總結(jié)分析了時態(tài)邏輯建模語言(Temporal Trace Language,TTL)的相關(guān)特征,概括性地介紹了Agent的理論基礎(chǔ)和Multi-Agent的系統(tǒng)構(gòu)建特征,并闡述了利用TTL語言對Multi-Agent系統(tǒng)進行形式化建模的方法。借鑒Wickens提出的人類信息加工模型,加入管制運行的相關(guān)要素,并根據(jù)場景角色的交互特征建立響應(yīng)執(zhí)行Multi-Agent系統(tǒng)模型,描述交互過程中Agent之間的關(guān)系。其次,針對建立的響應(yīng)執(zhí)行交互模型,從時態(tài)邏輯的角度出發(fā)構(gòu)建響應(yīng)執(zhí)行場景形式化模型與仿真模型。首先,對場景中涉及的相關(guān)靜態(tài)概念進行收集,然后抽象出屬性要素之間的動態(tài)關(guān)系,接著根據(jù)TTL的規(guī)范將概念、關(guān)系以及屬性形式化,最后,介紹了仿真建模語言(Language and Environment for Analysis of Dynamics by SimulaTi On,LEADSTO)語義、語法規(guī)則以及動態(tài)屬性關(guān)系構(gòu)建方法,并闡述了建模與仿真的具體步驟,包括模型概念化、形式化、仿真以及評估分析。以一種典型的跑道侵入事件中管制員響應(yīng)執(zhí)行場景為例,建立其時態(tài)邏輯模型,并構(gòu)建場景需要滿足的規(guī)則屬性,描述規(guī)則屬性之間的層級關(guān)系。選取此場景的不安全事件案例,對事件進行形式化建模、仿真建模以及邏輯推理分析,自動推理出事件軌跡中不滿足規(guī)則屬性的動態(tài)屬性,從而找出誘發(fā)事件發(fā)生的危險要素;再變更仿真案例中不同的屬性因子組合,進行仿真對比分析,抽象出誘發(fā)差錯和事件發(fā)生的多種因素,探索出阻止差錯和事件發(fā)生的有效措施,進而提出有效地緩解措施。結(jié)果表明,該方法能實現(xiàn)邏輯化、動態(tài)性的仿真,并通過形式化推理識別出事件中的危險要素,克服了單純利用自然語言進行危險分析的缺點,為后續(xù)此類事件的分析提供了科學的方法指導。
[Abstract]:Controller response is an important part of air traffic control, and it is also a key process of causing unsafe events in the operation of civil aviation air traffic control. In order to conduct an in-depth analysis of unsafe events involving controllers' response to the execution process, to improve the normative and automated level of event analysis and to avoid overusing the shortcomings of natural language descriptions, A formal reasoning method based on temporal logic is proposed. Firstly, this paper summarizes and analyzes the relevant features of temporal logic modeling language (Temporal Trace Language,TTL), introduces the theoretical basis of Agent and the characteristics of Multi-Agent system construction, and expounds the formal modeling method of Multi-Agent system using TTL language. Based on the human information processing model proposed by Wickens, this paper adds the relevant elements of control operation, and establishes the response execution Multi-Agent system model according to the interaction characteristics of scene roles, and describes the relationship between Agent in the process of interaction. Secondly, based on the response execution interaction model, the formal model and simulation model of response execution scenario are constructed from the point of view of temporal logic. First, the static concepts involved in the scene are collected, then the dynamic relations between attribute elements are abstracted, then the concepts, relationships and attributes are formalized according to the TTL specification. Finally, This paper introduces the semantics, syntax rules and dynamic attribute relation construction method of simulation modeling language (Language and Environment for Analysis of Dynamics by SimulaTi On,LEADSTO), and expounds the concrete steps of modeling and simulation, including model conceptualization, formalization, simulation and evaluation analysis. Taking a typical runway intrusion event as an example, the temporal logic model of controller response execution scene is established, and the rule attributes that need to be satisfied in the scene are constructed to describe the hierarchical relationship between the rules attributes. This paper selects the unsafe event case of this scene, carries on the formalization modeling, the simulation modeling and the logical reasoning analysis to the event, automatically inferences the dynamic attribute which does not satisfy the rule attribute in the event track, thus finds out the dangerous factor which induces the event to occur; Then changing the different attribute factor combination in the simulation case, comparing and analyzing the simulation, abstracting various factors that induce errors and events, exploring effective measures to prevent errors and events, and then putting forward effective mitigation measures. The results show that the method can realize logical and dynamic simulation, and identify the dangerous elements in the event by formal reasoning, which overcomes the disadvantage of using natural language to carry out hazard analysis. It provides scientific guidance for the analysis of this kind of events.
【學位授予單位】：中國民航大學
【學位級別】：碩士
【學位授予年份】：2016
【分類號】：V355.1

【相似文獻】

相關(guān)期刊論文 前10條

1 杜慧敏,韓俊剛,高德遠;用于描述和驗證數(shù)字電路的一階間隔時態(tài)邏輯[J];西北工業(yè)大學學報;1999年01期

2 田國會，劉長有，，徐心和;分揀系統(tǒng)運行過程的時態(tài)邏輯描述與分析[J];計算機集成制造系統(tǒng)-CIMS;1997年04期

3 韓俊剛;硬件設(shè)計的形式驗證與時態(tài)邏輯[J];計算機輔助設(shè)計與圖形學學報;1990年01期

4 楊惠珍,康鳳舉,馬裕民,蔡斌;基于時態(tài)邏輯的形式化聯(lián)邦校核方法[J];西北工業(yè)大學學報;2005年04期

5 田國會,徐心和,劉長有;自動化倉庫客戶服務(wù)管理問題的時態(tài)邏輯描述[J];東北大學學報;1997年06期

6 唐達,徐超,楊曉麗;工作流建模中時態(tài)邏輯的研究與應(yīng)用[J];計算機集成制造系統(tǒng)-CIMS;2004年04期

7 杜慧敏,楊紅麗,高德遠,韓俊剛;一種基于時態(tài)邏輯的有限狀態(tài)系統(tǒng)驗證方法[J];西北工業(yè)大學學報;2000年01期

8 樂全明;董志峗;鄭華珍;郁惟鏞;張沛超;王忠民;章啟明;;基于時態(tài)邏輯技術(shù)的高壓輸電線系統(tǒng)故障診斷[J];電力系統(tǒng)自動化;2006年09期

9 肖美華,薛錦云;時態(tài)邏輯形式化描述并發(fā)系統(tǒng)性質(zhì)[J];海軍工程大學學報;2004年05期

10 賁可榮，陳火旺;PTL證明器的實現(xiàn)技術(shù)[J];國防科技大學學報;1994年01期

相關(guān)會議論文 前5條

1 田國會;劉長有;徐心和;;離散事件動態(tài)系統(tǒng)理論的時態(tài)邏輯研究方法[A];1996中國控制與決策學術(shù)年會論文集[C];1996年

2 田國會;劉長有;徐心和;;電梯服務(wù)系統(tǒng)的時態(tài)邏輯描述、分析與控制[A];1996年中國控制會議論文集[C];1996年

3 陳玉泉;陳宣;陸汝占;;內(nèi)涵時態(tài)邏輯的語義解釋系統(tǒng)[A];自然語言理解與機器翻譯——全國第六屆計算語言學聯(lián)合學術(shù)會議論文集[C];2001年

4 李曉鷗;郭令忠;徐心和;;Petri網(wǎng)監(jiān)控的時態(tài)邏輯框架[A];1994中國控制與決策學術(shù)年會論文集[C];1994年

5 劉新;鄒麗;;直覺模糊時態(tài)邏輯[A];模糊集理論與應(yīng)用——98年中國模糊數(shù)學與模糊系統(tǒng)委員會第九屆年會論文選集[C];1998年

相關(guān)博士學位論文 前1條

1 呂嘉;基于開放時態(tài)邏輯的面向方面程序形式化驗證和模塊推理研究[D];浙江大學;2009年

相關(guān)碩士學位論文 前8條

1 田潔;基于時態(tài)邏輯的管制員響應(yīng)執(zhí)行差錯建模與分析方法研究[D];中國民航大學;2016年

2 劉冬寧;時態(tài)邏輯及其對知識庫的構(gòu)架與研究[D];廣東工業(yè)大學;2004年

3 李嵐;略論時態(tài)邏輯在計算機科學中的發(fā)展[D];華東師范大學;2013年

4 李學軍;基于時態(tài)邏輯的遷移實例運行時安全研究[D];山東大學;2009年

5 王勝;基于SystemC的時態(tài)邏輯屬性驗證方法研究[D];北京化工大學;2009年

6 趙峗;基于時態(tài)邏輯的UML交互模型檢測研究[D];青島大學;2008年

7 白金山;二元判斷圖BDD及其JAVA實現(xiàn)的應(yīng)用與研究[D];貴州大學;2008年

8 張紅軍;一類對象Petri網(wǎng)建模與驗證方法研究[D];鄭州大學;2006年

本文編號：2209325