Esta Tese apresenta uma contribuição para avaliação da comunicação digital na operação de veículos aéreos não tripulados (VANT) no ambiente aeronáutico. A comunicação digital aeronáutica relaciona-se diretamente ao nível de segurança crítica desejado para o controle do fluxo de tráfego aéreo, por parte de autoridades e de órgãos normativos, os quais possuem como objetivo tornar a comunicação uniforme para todos os continentes. Diversas são as discussões acerca do nível de segurança crítica que a comunicação digital entre VANT e controle em terra possa exibir, sempre buscando redução da exposição a riscos inerentes à operação desse tipo de veículo. Nesse contexto, a proposta desta Tese é avaliar a segurança na comunicação digital, por meio do uso de injeção de falhas, para operações de veículos aéreos não tripulados. Este trabalho descreve a importância de analisar as interferências causadas por falhas na comunicação digital, relacionadas ao envio de mensagens entre o órgão de controle e a aeronave não tripulada. Também são definidos quais os tipos de falhas que causam um maior impacto na comunicação, bem como quais os parâmetros que devem ser utilizados para manipulação das variáveis de falhas na comunicação. Para atender a avaliação proposta, foi utilizado o ambiente simulado que reúne as características do ambiente aeronáutico, denominado PipE-SEC (Plataforma Integrada para Ensaios de Sistemas Embarcados Críticos), bem como o protocolo CPDLC (Controller-Pilot Data Link Communications) para troca de mensagens digitais. / This thesis presents a contribution to the evaluation of digital communication in the operation of unmanned aerial vehicles (UAV) in the aeronautical environment. Aeronautical digital communication relates directly to the critical safety level required for controlling the air traffic flow by authorities and regulatory agencies, which are aimed at making communication uniform for all continents. There are several discussions about the safety critical level that digital communication between UAVs and ground control can display, always seeking to reduce exposure to risks inherent in the operation of such vehicles. In this context, the proposal of this thesis is to evaluate the safety in digital communication, through the use of fault injection for operations of UAV. This work describes the importance of analyzing the interference caused by faults in digital communication related to sending messages between the control agency and the UAV. There are also defined what types of faults cause a greater impact on communication as well as which parameters should be used to simulate communication faults. To answer the proposed evaluation, we used the simulated environment that combines the features of the aeronautical environment, called PIpE-SEC (Integrated Platform for Test Critical Embedded Systems), as well as the protocol CPDLC (Controller-Pilot Data Link Communications) to exchange digital messages.

Com o objetivo da redução do tempo de desenvolvimento de produtos comerciais, hardwares padronizados, como microcontroladores e microprocessadores dedicados, têm sido largamente empregados em aplicações críticas, transferindo para o software elementos até então de responsabilidade exclusiva do hardware. Técnicas de programação defensiva são mecanismos preventivos contra a ocorrência de falhas de hardware ou de software. Para a verificação da segurança de sistemas de aplicações críticas, técnicas de injeção de falhas foram desenvolvidas, propiciando o teste dos mecanismos de tolerância a falhas em condições muito semelhantes às do ambiente operacional real. A introdução de técnicas de programação defensiva aumenta a segurança dos sistemas de aplicações críticas. Não há, na literatura pesquisada, qualquer referência a uma avaliação quantitativa das técnicas de programação defensiva. Esta tese é a descrição de um trabalho experimental, que visa esta avaliação quantitativa, e se organiza em algumas etapas. Primeiro, algumas técnicas de programação defensiva são apresentadas, caracterizadas e eleitas como objeto de avaliação. A seguir, técnicas de injeção de falhas são descritas e uma delas é eleita como meio de teste do trabalho experimental. A partir daí, as técnicas de programação defensiva são verificadas sob o enfoque da técnica de injeção de falhas escolhida. O resultado é uma avaliação quantitativa relativa da eficácia de algumas técnicas de programação defensiva na capacidade de tolerância a falhas inseguras de sistemas de aplicações críticas. Ao final, indicações de continuidade do trabalho são apresentadas. O ambiente metroferroviário, em que trabalha o autor, foi utilizado como estudo de caso. Entretanto, as considerações e conclusões desta tese se aplicam a qualquer sistema de missão critica. / Aiming the reduction of commercial systems` time to the market, standardized hardware, as microcontrollers and embedded microprocessors, has been broadly employed for critical applications, transferring to the software issues that once exclusively relied on the hardware design. Defensive programming techniques are preventive engines against hardware and software faults. In order to verify the safety of critical application systems, fault injection techniques were developed, allowing for the testing of fault tolerant techniques under conditions quite close to actual operational environments. The introduction of defensive programming techniques increases the safety of critical application systems. There are no references, on a large research base, on quantitative evaluations of defensive programming techniques. This thesis describes an experimental work towards a relative quantitative evaluation, organized in a few stages. First, some defensive programming techniques are shown, characterized and selected as the evaluation target. Following, fault injection techniques are described and one of them is selected as the agent of the experimental work. From this point on, the defensive programming techniques are verified under the fault injection technique chosen. The result is a relative quantitative evaluation on the efficiency of some defensive programming techniques on the unsafe fault tolerance capacity of critical application systems. Finally, indications for further work are presented. The railway environment, where the author works, was employed as a case study. However, the reasoning and the conclusions of this thesis are applicable to any critical mission system.

Com o objetivo da redução do tempo de desenvolvimento de produtos comerciais, hardwares padronizados, como microcontroladores e microprocessadores dedicados, têm sido largamente empregados em aplicações críticas, transferindo para o software elementos até então de responsabilidade exclusiva do hardware. Técnicas de programação defensiva são mecanismos preventivos contra a ocorrência de falhas de hardware ou de software. Para a verificação da segurança de sistemas de aplicações críticas, técnicas de injeção de falhas foram desenvolvidas, propiciando o teste dos mecanismos de tolerância a falhas em condições muito semelhantes às do ambiente operacional real. A introdução de técnicas de programação defensiva aumenta a segurança dos sistemas de aplicações críticas. Não há, na literatura pesquisada, qualquer referência a uma avaliação quantitativa das técnicas de programação defensiva. Esta tese é a descrição de um trabalho experimental, que visa esta avaliação quantitativa, e se organiza em algumas etapas. Primeiro, algumas técnicas de programação defensiva são apresentadas, caracterizadas e eleitas como objeto de avaliação. A seguir, técnicas de injeção de falhas são descritas e uma delas é eleita como meio de teste do trabalho experimental. A partir daí, as técnicas de programação defensiva são verificadas sob o enfoque da técnica de injeção de falhas escolhida. O resultado é uma avaliação quantitativa relativa da eficácia de algumas técnicas de programação defensiva na capacidade de tolerância a falhas inseguras de sistemas de aplicações críticas. Ao final, indicações de continuidade do trabalho são apresentadas. O ambiente metroferroviário, em que trabalha o autor, foi utilizado como estudo de caso. Entretanto, as considerações e conclusões desta tese se aplicam a qualquer sistema de missão critica. / Aiming the reduction of commercial systems` time to the market, standardized hardware, as microcontrollers and embedded microprocessors, has been broadly employed for critical applications, transferring to the software issues that once exclusively relied on the hardware design. Defensive programming techniques are preventive engines against hardware and software faults. In order to verify the safety of critical application systems, fault injection techniques were developed, allowing for the testing of fault tolerant techniques under conditions quite close to actual operational environments. The introduction of defensive programming techniques increases the safety of critical application systems. There are no references, on a large research base, on quantitative evaluations of defensive programming techniques. This thesis describes an experimental work towards a relative quantitative evaluation, organized in a few stages. First, some defensive programming techniques are shown, characterized and selected as the evaluation target. Following, fault injection techniques are described and one of them is selected as the agent of the experimental work. From this point on, the defensive programming techniques are verified under the fault injection technique chosen. The result is a relative quantitative evaluation on the efficiency of some defensive programming techniques on the unsafe fault tolerance capacity of critical application systems. Finally, indications for further work are presented. The railway environment, where the author works, was employed as a case study. However, the reasoning and the conclusions of this thesis are applicable to any critical mission system.

Esta Tese apresenta uma contribuição para avaliação da comunicação digital na operação de veículos aéreos não tripulados (VANT) no ambiente aeronáutico. A comunicação digital aeronáutica relaciona-se diretamente ao nível de segurança crítica desejado para o controle do fluxo de tráfego aéreo, por parte de autoridades e de órgãos normativos, os quais possuem como objetivo tornar a comunicação uniforme para todos os continentes. Diversas são as discussões acerca do nível de segurança crítica que a comunicação digital entre VANT e controle em terra possa exibir, sempre buscando redução da exposição a riscos inerentes à operação desse tipo de veículo. Nesse contexto, a proposta desta Tese é avaliar a segurança na comunicação digital, por meio do uso de injeção de falhas, para operações de veículos aéreos não tripulados. Este trabalho descreve a importância de analisar as interferências causadas por falhas na comunicação digital, relacionadas ao envio de mensagens entre o órgão de controle e a aeronave não tripulada. Também são definidos quais os tipos de falhas que causam um maior impacto na comunicação, bem como quais os parâmetros que devem ser utilizados para manipulação das variáveis de falhas na comunicação. Para atender a avaliação proposta, foi utilizado o ambiente simulado que reúne as características do ambiente aeronáutico, denominado PipE-SEC (Plataforma Integrada para Ensaios de Sistemas Embarcados Críticos), bem como o protocolo CPDLC (Controller-Pilot Data Link Communications) para troca de mensagens digitais. / This thesis presents a contribution to the evaluation of digital communication in the operation of unmanned aerial vehicles (UAV) in the aeronautical environment. Aeronautical digital communication relates directly to the critical safety level required for controlling the air traffic flow by authorities and regulatory agencies, which are aimed at making communication uniform for all continents. There are several discussions about the safety critical level that digital communication between UAVs and ground control can display, always seeking to reduce exposure to risks inherent in the operation of such vehicles. In this context, the proposal of this thesis is to evaluate the safety in digital communication, through the use of fault injection for operations of UAV. This work describes the importance of analyzing the interference caused by faults in digital communication related to sending messages between the control agency and the UAV. There are also defined what types of faults cause a greater impact on communication as well as which parameters should be used to simulate communication faults. To answer the proposed evaluation, we used the simulated environment that combines the features of the aeronautical environment, called PIpE-SEC (Integrated Platform for Test Critical Embedded Systems), as well as the protocol CPDLC (Controller-Pilot Data Link Communications) to exchange digital messages.

Submitted by Cláudia Bueno (claudiamoura18@gmail.com) on 2015-12-03T14:15:36Z No. of bitstreams: 2 Dissertação - Andesson Brito Nascimento - 2015.pdf: 4640566 bytes, checksum: dbcca8bfca43a95c51641cfa230b0285 (MD5) license_rdf: 23148 bytes, checksum: 9da0b6dfac957114c6a7714714b86306 (MD5) / Approved for entry into archive by Luciana Ferreira (lucgeral@gmail.com) on 2015-12-04T06:59:29Z (GMT) No. of bitstreams: 2 Dissertação - Andesson Brito Nascimento - 2015.pdf: 4640566 bytes, checksum: dbcca8bfca43a95c51641cfa230b0285 (MD5) license_rdf: 23148 bytes, checksum: 9da0b6dfac957114c6a7714714b86306 (MD5) / Made available in DSpace on 2015-12-04T06:59:29Z (GMT). No. of bitstreams: 2 Dissertação - Andesson Brito Nascimento - 2015.pdf: 4640566 bytes, checksum: dbcca8bfca43a95c51641cfa230b0285 (MD5) license_rdf: 23148 bytes, checksum: 9da0b6dfac957114c6a7714714b86306 (MD5) Previous issue date: 2015-07-24 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior - CAPES / Correlations are ubiquitous in nature and have played an extremely important role in human life for a long time. For example, in economy, correlations between price and demand are extremely important for a businessman (or even a government) to make decisions regarding their investment policy. In the field of biology, genetic correlations are central to follow individual characteristics. The relationship between income distribution and crime rate is just one example coming from the social sciences. Mathematically, correlation is a number that describes the degree of relationship between two variables. In the classical domain, this number can be computed in the context of information theory, developed by Shannon in 1948. Focusing on the subject of the present work, the discussion regarding the quantum nature of the correlations permeates physics since Einstein, Podolski and Rosen published their famous article criticizing quantum mechanics. Since then, the so-called quantum correlations have been shown to be a very important tool in the study of many-bodies physics. Another feature of many-body physics is that certain systems, under certain conditions, exhibit what we call quantum phase transition. Such transitions are analogous to the classical transitions, but being governed by purely quantum fluctuations and, as such, may occur at zero temperature, unlike the former, which are guided by thermal fluctuations. One of the main phenomenon that characterizes these transitions is the fact that the correlation length (defined between two subsystems of the global system) highly increases at the transition point. This means that such subsystems can be strongly correlated even if they are separated by a large distance. The main goal of the present work is the study of quantum correlations, specifically the entanglement and the local quantum uncertainty (LQU), in systems presenting one or more quantum phase transitions. Specifically, we consider three models of spin chains: 1) The XY and the XY T, which describes chains of spins- 1=2 —the second considering three spins interaction while the first one takes into account only pairwise interactions; 2) A model describing a chain formed by bosonic spins, i.e. particles with spin-1. As a general conclusion, quantum correlation provides a very powerful tool for the study of critical phenomena, providing, among other things, a means to identify a quantum phase transition. / As correlações são onipresentes na natureza e têm desempenhado um papel extremamente importante na vida humana por um longo tempo. Por exemplo, na economia correlações entre oferta e demanda são extremamente importantes para um homem de negócios (ou mesmo para um governo) tomar decisões à respeito de sua política de investimento. No campo da biologia, correlações genéticas são fundamentais para seguirmos características individuais. A relação entre distribuição de renda e taxa de criminalidade é apenas um dos exemplo vindos das Ciências Sociais. De um modo geral, a correlação é uma quantidade que descreve o grau de relação entre duas variáveis. No domínio clássico, essa quantidade pode ser medida no âmbito da teoria da informação, desenvolvida por Shannon em 1948. Focando no assunto do presente trabalho, a discussão sobre a natureza quântica das correlações permeia a física desde que Einstein, Podolski e Rosen publicaram seu famoso artigo criticando a mecânica quântica. Desde então, as chamadas correlações quânticas têm se mostrado uma ferramenta muito importante no estudo da Física de muitos corpos. Outra característica da Física de muitos corpos é que certos sistemas, em certas condições, exibem o que chamamos de transição de fase quântica. Tais transições são análogas às transições clássicas, mas sendo governadas por flutuações de natureza puramente quântica, podendo ocorrer à temperatura zero, ao contrário das primeiras, que são guiadas por flutuações térmicas. Um dos principais fenômenos que caracterizam estas transições é o fato de que o comprimento de correlação (definido entre dois subsistemas do sistema global) torna-se de longo alcance no ponto de transição. Isso significa que tais subsistemas podem estar fortemente correlacionados mesmo estando separados por uma grande distância. O objetivo deste trabalho é o estudo de correlações quânticas, mais especificamente do emaranhamento e da incerteza local quântica (LQU), em cadeias de spin que apresentem uma ou mais transições quânticas de fase. Especificamente, estudamos três modelos de cadeias de spin: Os modelos XY e XY T, que são cadeias formadas por spins-1=2, sendo que o segundo considera interação entre três spins enquanto o primeiro somente entre pares; um modelo formado por partículas bosônicas de spin-1. Como conclusão geral, temos que as correlações quânticas fornecem uma ferramenta muito boa para o estudo de fenômenos críticos, oferecendo, entre outros, um meio de identificarmos uma transição quântica de fase.

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.

At safety-critical, mission-critical and business-critical systems the high cost of failure makes required the use of methods and techniques to ensure application reliability. In this context, formal languages, as Circus or specific languages versions like Safety-Critical Java, were created to facilitate the verification and validation of applications so consequently assisting to increase the overall reliability. Despite of the reliability increase, the modeled systems in formal languages can not be executed subsequently has to be implemented in a traditional programming language. It is in this process of free translation where occur most mistakes that end up not ensuring that the generated code conforms to the specification. Based on that premise, this paper propose to expound a strategy of translation from models written in Circus language to executable programs in SCJ language. Among the main objectives and contributions include the creation of EBNFs of the two languages and the detailed description of the translation of all elements between the two languages. / Em sistemas críticos de segurança, missão ou negócios o alto custo das falhas faz com que sejam necessários o uso de métodos e técnicas para garantir a confiabilidade da aplicação. É neste contexto que foram criadas linguagens formais como o Circus ou versões específicas de linguagens como o Safety-Critical Java para facilitar a verificação e validação das aplicações criadas e aumentar consequentemente a confiabilidade geral da aplicação. Apesar de aumentar a confiabilidade, os sistemas modelados em linguagens formais não podem ser executados e então precisam ser implementados em uma linguagem de programação tradicional. É nesse processo de livre tradução do sistema especificado onde ocorrem a maioria dos erros que acabam por não garantir que o código gerado esteja de acordo com a especificação. Baseando-se nessa premissa o presente trabalho propõem-se a apresentar uma estratégia de tradução de modelos escritos na linguagem Circus para programas executáveis na linguagem SCJ. Entre os principais objetivos e contribuições do trabalho estão a criação das EBNFs das duas linguagens e a descrição detalhada da tradução de todos os elementos entre as duas linguagens.

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.