No description available.

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.

Modern traffic management systems often rely on static technologies, such as sensors and CCTV-cameras, in the gathering of data regarding the current traffic situation. Recent reports have shown that this method can result in a lack of coverage in Stockholm, Sweden. In addressing this issue, an alternative strategy to installing more sensors and CCTV-cameras could be to utilize crowdsourced traffic data from other sources, such as Waze. In order to examine the usage and potential utility of crowdsourced data in traffic management, the Swedish Transport Administration’s center in Stockholm, Trafik Stockholm, developed a web application which visualizes traffic data from both official sources and Waze. While the application was successful in doing so, it revealed the problem of integrating the traffic data from these two sources, as a significant portion of the data was redundant, and the reliability occasionally was questionable. This study aims at determining how issues regarding redundancy and reliability can be resolved in the integration of crowdsourced and official traffic data. Conducted using a design science research strategy, the study investigates these issues by designing and developing an artifact that implements integration methods to match alerts from the data sources based on temporal and spatial proximity constraints. The artifact was evaluated through test sessions in which real-time traffic data from all over Sweden was processed, and through acceptance testing with the stakeholders of the application. Analysis of the results from the evaluations shows that the artifact is effective in reducing the redundancy in the crowdsourced data and that it can provide a more solid ground for reliability assessment. Furthermore, the artifact met its expectations and requirements, demonstrating a proof-of-concept and a proof-of-acceptance. Based on these results, the study concludes that by analyzing temporal and spatial factors in crowdsourced data, redundancy issues in the integration of crowdsourced and official traffic can be resolved to a large extent. Furthermore, it is concluded that reliability issues in the same context can be resolved to a high degree by managing redundancy factors in combination with general traffic management factors. While the study is focused on traffic management, the issues of redundancy and reliability are not restricted to crowdsourced data in this context specifically. Thus, the results of the study are potentially of interest to researchers investigating other areas of application for crowdsourcing as well.

Originally presented as the author's Thesis (doctoral)--Technische Universität München. / "FGV-TUM." Includes bibliographical references (p. 147-156).

Originally presented as the author's Thesis (doctoral)--Technische Universität München. / "FGV-TUM." Includes bibliographical references (p. 147-156).

Master of Science

<p dir="ltr">Traffic Incident Management (TIM) is an important tool for agencies to reduce secondary crashes, improve travel reliability, and ensure safety of first responders. Having “eyes” on the scene from roadside traffic cameras can assist operators to dispatch appropriate personnel, provide situational awareness, and allow for quick response when incident conditions change. Many intelligent traffic systems (ITS) centers deploy pan-tilt-zoom (PTZ) cameras that provide broad coverage but require operators to position. When incidents occur or a public safety vehicle stops for roadside assistance, Traffic Management Center (TMC) operators need to reposition cameras to monitor the event. The camera positioning time depends on operator experience, accuracy of 911 call, location, public safety radio reports, and in some cases, GPS positions. This research outlines the methodology to use GPS data sources to automate camera position to a scene for event nature verification. In general, this GPS information can come from either connected vehicles or public safety vehicles, such as Indiana Department of Transportation (INDOT) Hoosier Helpers. Implementing this research into INDOT daily operations has increased the number of events that cameras verify, while decreasing the time from event occurrence to camera verification from a median of 5 minutes to a median of approximately 90 seconds. The time is driven by the accuracy and frequency of GPS data from devices. With increased telematics polling rates and availability of enhanced vehicle data such as door open/close and seatbelt latch events, this latency is expected to further decline. </p>

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.