Use este identificador para citar ou linkar para este item:
http://hdl.handle.net/1843/ESBF-AEHPXF| Tipo: | Tese de Doutorado |
| Título: | Verification of vehicular networks using probabilistic model checking |
| Autor(es): | Bruno Ferreira |
| Primeiro Orientador: | Sergio Vale Aguiar Campos |
| Primeiro Coorientador: | Antonio Alfredo Ferreira Loureiro |
| Primeiro membro da banca : | Antonio Alfredo Ferreira Loureiro |
| Segundo membro da banca: | Jose Marcos Silva Nogueira |
| Terceiro membro da banca: | Leila Ribeiro |
| Quarto membro da banca: | Mark Alan Junho Song |
| Resumo: | Redes Veiculares ou VANETs (do inglês vehicular ad-hoc networks) são um tipo particular de redes móveis ad hoc, ou seja, caracterizadas pela ausência de um elemento centralizador durante a transmissão. VANETs são formadas por comunicação wireless entre os próprios veículos ou entre os automóveis e elementos fixos dispostos em avenidas ou rodovias. Existem vários tipos de aplicações possíveis e um bom exemplo são os semáfaros virtuais ou VTL (Virtual Traffic Light). Esses sinais virtuais são implementados de uma maneira distribuída pelos veículos, assim, a temporização pode ser adaptada com respeito ao volume do tráfego atual de cada via. Essa técnica mostrou resultados animadores no controle do trânsito. Ela é capaz de melhorar o fluxo do tráfego e reduzir o custo com infraestrutura. Contudo, essa aplicação e muitas outras em VANET ainda tem grandes desafios para sua ampla adoção. Uma interessante questão é como elas serão testadas de forma realística. Simulação é amplamente utilizada a fim de minimizar custos e reduzir o tempo dos experimentos, uma vez que não são necessários elementos físicos e os testes pode ser facilmente reproduzidos.As áreas de redes de computadores e a de engenharia de tráfego estão fazendo uso extensivo de simuladores, assim, existem software consagrados em ambas as áreas. Contudo, à partir da introdução das redes veiculares, a integração entre esses dois tipos de simuladores vem sendo necessária. Tal interação é requerida devido à característica inerente entre o forte acoplamento da rede de comunicação e a mobilidade em VANETs. Aplicações podem alterar os padrões de mobilidade que por sua vez, podem distorcer a comunicação de dados entre os veículos, afastando ou agrupando-os. Por isso, existe uma relação bidirecional forte entre comunicação e movimento em redes veiculares.No entanto, a maioria dos simuladores de redes e tráfego ainda usam um abordagem de interação isolada, ou seja, eles não trocam informações em tempo real. Outra técnica usa um software para conectar os simuladores e proporcionam uma interação. Mas essa técnica sofre com requisitos de latência, devido a sincronização entre eles. Além disso, o custo computacional é caro, pois ambos simuladores devem ser executados simultaneamente. Outras questões surgem porque muitos software responsáveis por representar as redes ainda não suportam os dispositivos e camadas de protocolos propostos pelas VANETs.Contudo, uma outra técnica é a análise formal utilizando verificação de modelos probabilística ou PMC (probabilistic model checking), a qual explora um modelo de forma automática e exaustiva verificando se uma propriedade é satisfeita utilizando um tipo especial de lógica. Estudos preliminares mostram que verificação de modelos vem sendo utilizados para analisar redes de sensores sem fios e VANETs. Eles consideram importantes questões como o não determinismo durante a transmissão das mensagem. Mas, o tráfego veicular, a rede de computadores e a propagação de sinal são necessários e raramente explorados nesta área.Deste modo, esse trabalho propõem-se a fornecer diretrizes para verificar redes veiculares utilizando PMC. Trabalhos futuros podem usar as instruções propostas aqui para analisar protocolos em VANET ou para construir uma ferramenta que automatize a criação de modelo para tais análises. Essas diretrizes podem servir como complemento à simulação no estudo das redes veiculares.Assim, um modelo microscópico, o qual representa o fluxo de tráfego em detalhes e um modelo estocástico que representa a possibilidade de receber uma mensagem com uma probabilidade p são considerados em nossas diretrizes. A fim de ilustrar o modelo proposto, aplicações e protocolos em VANET são apresentados estudados. Assim, a tese apresenta os conceitos necessários como verificação de modelos, redes veiculares. Os modelos analíticos usados nas diretrizes também são apresentados. Além disso, alguns modelos experimentais são implementados com os conceitos destacados e finalmente, nossas diretrizes são para a modelagem desses modelos em VANET são apresentadas. |
| Abstract: | Vehicular Ad-hoc Networks (VANETs) are a particular case of mobile network in which nodes are vehicles using wireless communication among themselves and/or fixed controllers deployed on streets. However, VANETs have yet great challenges. An interesting question is how will they be tested? Simulation is widely used in order to minimize costs, however it suffers with problems such as the realistic interaction between networks and traffic flow. Thus, another approach is the formal verification through Probabilistic Model Checking (PMC), a technique that automatically and exhaustively explores a model, verifying if it satisfies properties given in special types of logics. We have been proposing guidelines for verifying VANETs through PCM. For this, a microscopic model, which describes the traffic flow and represents the possibility to receive a message with a certain probability is considered. Nevertheless, this thesis presents the proposed guideline to model VANET in a complete way. |
| Assunto: | Vehicular ad hoc network Mobile ad hoc network Probabilistic model checking Computação |
| Idioma: | Inglês |
| Editor: | Universidade Federal de Minas Gerais |
| Sigla da Instituição: | UFMG |
| Tipo de Acesso: | Acesso Aberto |
| URI: | http://hdl.handle.net/1843/ESBF-AEHPXF |
| Data do documento: | 9-Set-2016 |
| Aparece nas coleções: | Teses de Doutorado |
Arquivos associados a este item:
| Arquivo | Descrição | Tamanho | Formato | |
|---|---|---|---|---|
| brunoferreira.pdf | 6.06 MB | Adobe PDF | Visualizar/Abrir |
Os itens no repositório estão protegidos por copyright, com todos os direitos reservados, salvo quando é indicado o contrário.