Thesis (MEng)--Stellenbosch University, 2015. / ENGLISH ABSTRACT: Increasing air traffic and urbanisation has led to a cluttered airspace, particularly near airports, where both complex terrain and multiple moving obstacles are frequent. Accurately and efficiently predicting violations in safe separation criteria for commercial aircraft, a process called conflict detection, is therefore crucial in assessing risk associated with threats of collision. Existing avoidance systems in operation such as TCAS, EGPWS and ATC exhibit shortcomings, leaving room for uncertainty and possible conflict scenarios. A single on-board system capable of minimising errors in prediction would inform conflict resolution decisions more accurately as well as support the notion of free flight, an objective of next-generation air traffic management systems. This thesis investigates the viability of a modern algorithm, probability flow, as a method of probabilistic conflict detection for commercial aircraft in airport environments. Simulation results for realistic flight scenarios are presented in comparison with a ground-truth result obtained through Monte Carlo simulation. Observations are made regarding the suitability of probability flow for real-world application. It is found that probability flow is capable of calculating a tight upper bound to the probability of conflict quickly and accurately for most conflict scenarios. However, unreasonably large overestimates on the probability of conflict are obtained when flying parallel to an obstacle conflict region. This problem could lead to a high frequency of false alerts, particularly in aborted landing scenarios and at airports operating parallel runways. It is therefore advised that further research be conducted to resolve this problem before probability flow can be reliably implemented in an airport environment. / AFRIKAANSE OPSOMMING: Toenemende lugverkeer en verstedeliking het gelei tot ‘n deurmekaar lugruim, veral naby lughawens, waar beide komplekse terrein en verskeie bewegende struikelblokke gereeld voorkom. Akkuraat en doeltreffende voorspelling van oortredings in veilige skeidingskriteria vir kommersiële vliegtuie, naamlik konflik opsporing, is dus van kardinale belang in die beoordeling van die risiko wat verband hou met dreigemente van ‘n botsing. Bestaande vermyding stelsels in werking soos TCAS, EGPWS en ATC toon tekortkominge, wat ruimte laat vir onsekerheid en moontlike konflik scenario’s. ‘n Enkele aanboordstelsel, wat in staat is om foute in voorspelling te verminder, sou konflikresolusie besluite meer akkuraat in kennis stel, asook om die idee van vrye vlug te ondersteun, ‘n doelwit van toekomstige lugverkeer beheerstelsels. Hierdie tesis ondersoek die lewensvatbaarheid van ‘n moderne algoritme, waarskynlikheidsvloei, as ‘n metode van probabilistiese konflik opsporing vir kommersiële vliegtuie in die lughawens omgewing. Simulasie resultate vir realistiese vlug scenario’s word aangebied in vergelyking met ‘n grond-waarheid resultaat wat verkry word deur middel van Monte Carlo simulasie. Waarnemings word gemaak ten opsigte van die geskiktheid van waarskynlikheidsvloei vir die werklikheid. Dit is bevind dat waarskynlikheidsvloei in staat is om die berekening van ‘n stywe bogrens tot die waarskynlikheid van konflik vinnig en akkuraat te bepaal vir die meeste konflik scenario’s. Tog is daar ‘n onredelike groot oorskatting op die waarskynlikheid van konflik wat verkry word wanneer ‘n vliegtuig parallel met ‘n hindernis konflik streek vlieg. Hierdie probleem kan lei tot ‘n hoë frekwensie van valse waarskuwings, veral in mislukte landing scenario’s en by lughawens wat van parallel aanloopbane gebruik maak. Dit word dus aanbeveel dat verdere navorsing gedoen word om die probleem op te los voordat waarskynlikheidsvloei betroubaar in ’n lughawe omgewing geïmplementeer word.

A evolução de sistemas de gerenciamento de tráfego aéreo é pesquisada para suportar o crescimento na demanda por transporte aéreo. Uma alternativa para essa evolução é o aumento no grau de automação. Os sistemas automatizados precisam ser tão seguros quanto os sistemas em operação atualmente. Com o uso de técnicas de especificação e verificação formal é possível avaliar os requisitos de sistemas. Neste trabalho, é proposto um ciclo de especificação formal, que consiste em um conjunto de diretrizes para aplicação de técnicas de métodos formais em requisitos escritos em linguagem natural. O resultado esperado da aplicação deste ciclo é um conjunto de requisitos escritos em linguagem natural verificados formalmente. O ciclo é composto pelas etapas: levantamento de requisitos do sistema e classificação em padrões de especificação; mapeamento dos requisitos para as linguagens de especificação formal LTL (Linear Temporal Logic) e CTL (Computation Tree Logic); verificação formal da especificação com o verificador NuSMV; ajustes na especificação baseada nos resultados da verificação; ajustes nos requisitos baseados nos ajustes na especificação. As diretrizes propostas são definidas com a análise da verificação formal do Automated Airspace Concept (AAC), padrões de especificação e diretrizes para uso do verificador NuSMV. Os resultados esperados são obtidos na aplicação do ciclo de especificação em dois estudos de caso. A principal contribuição do trabalho é o conjunto de diretrizes para elaboração de expressões escritas em linguagem de especificação formal baseadas em requisitos escritos em linguagem natural e que podem ser verificadas formalmente. / Air traffic management systems evolution is being researched to support air transportation demand growth. An evolution alternative is system automation degree increase. Automated systems need to be as safe as current operating systems. It is possible to analyze system requirements with the application of formal specification and formal verification techniques. In this work, a specification cycle is proposed. The specification cycle is a set of guidelines to use formal method techniques on requirements written in natural language. The specification cycle application expected result is a set of formally verified requirements written in natural language. This cycle is comprised of the following stages: system requirements elicitation and specification pattern classification; requirements mapping to LTL (Linear Temporal Logic) and CTL (Computation Tree Logic) formal specification languages; specification formal verification using the NuSMV verifier; formal specification adjustment based on verification results; requirements adjustment based on formal specification adjustment. The proposed guidelines are defined with the Automated Airspace Concept (AAC) formal verification analysis, specification patterns and guidelines for the NuSMV formal verifier use. The expected results are accomplished in the specification cycle application on two study cases. The main contribution of this work is the set of guidelines applied to formulate formally verifiable expressions specified in formal specification languages based on system requirements written in natural language.

A evolução de sistemas de gerenciamento de tráfego aéreo é pesquisada para suportar o crescimento na demanda por transporte aéreo. Uma alternativa para essa evolução é o aumento no grau de automação. Os sistemas automatizados precisam ser tão seguros quanto os sistemas em operação atualmente. Com o uso de técnicas de especificação e verificação formal é possível avaliar os requisitos de sistemas. Neste trabalho, é proposto um ciclo de especificação formal, que consiste em um conjunto de diretrizes para aplicação de técnicas de métodos formais em requisitos escritos em linguagem natural. O resultado esperado da aplicação deste ciclo é um conjunto de requisitos escritos em linguagem natural verificados formalmente. O ciclo é composto pelas etapas: levantamento de requisitos do sistema e classificação em padrões de especificação; mapeamento dos requisitos para as linguagens de especificação formal LTL (Linear Temporal Logic) e CTL (Computation Tree Logic); verificação formal da especificação com o verificador NuSMV; ajustes na especificação baseada nos resultados da verificação; ajustes nos requisitos baseados nos ajustes na especificação. As diretrizes propostas são definidas com a análise da verificação formal do Automated Airspace Concept (AAC), padrões de especificação e diretrizes para uso do verificador NuSMV. Os resultados esperados são obtidos na aplicação do ciclo de especificação em dois estudos de caso. A principal contribuição do trabalho é o conjunto de diretrizes para elaboração de expressões escritas em linguagem de especificação formal baseadas em requisitos escritos em linguagem natural e que podem ser verificadas formalmente. / Air traffic management systems evolution is being researched to support air transportation demand growth. An evolution alternative is system automation degree increase. Automated systems need to be as safe as current operating systems. It is possible to analyze system requirements with the application of formal specification and formal verification techniques. In this work, a specification cycle is proposed. The specification cycle is a set of guidelines to use formal method techniques on requirements written in natural language. The specification cycle application expected result is a set of formally verified requirements written in natural language. This cycle is comprised of the following stages: system requirements elicitation and specification pattern classification; requirements mapping to LTL (Linear Temporal Logic) and CTL (Computation Tree Logic) formal specification languages; specification formal verification using the NuSMV verifier; formal specification adjustment based on verification results; requirements adjustment based on formal specification adjustment. The proposed guidelines are defined with the Automated Airspace Concept (AAC) formal verification analysis, specification patterns and guidelines for the NuSMV formal verifier use. The expected results are accomplished in the specification cycle application on two study cases. The main contribution of this work is the set of guidelines applied to formulate formally verifiable expressions specified in formal specification languages based on system requirements written in natural language.