Verification of vehicular networks using probabilistic model checking

Bruno Ferreira

Please use this identifier to cite or link to this item: http://hdl.handle.net/1843/ESBF-AEHPXF

Full metadata record

DC Field	Value	Language
dc.contributor.advisor1	Sergio Vale Aguiar Campos	pt_BR
dc.contributor.advisor-co1	Antonio Alfredo Ferreira Loureiro	pt_BR
dc.contributor.referee1	Antonio Alfredo Ferreira Loureiro	pt_BR
dc.contributor.referee2	Jose Marcos Silva Nogueira	pt_BR
dc.contributor.referee3	Leila Ribeiro	pt_BR
dc.contributor.referee4	Mark Alan Junho Song	pt_BR
dc.creator	Bruno Ferreira	pt_BR
dc.date.accessioned	2019-08-13T21:59:09Z	-
dc.date.available	2019-08-13T21:59:09Z	-
dc.date.issued	2016-09-09	pt_BR
dc.identifier.uri	http://hdl.handle.net/1843/ESBF-AEHPXF	-
dc.description.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.	pt_BR
dc.description.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.	pt_BR
dc.language	Inglês	pt_BR
dc.publisher	Universidade Federal de Minas Gerais	pt_BR
dc.publisher.initials	UFMG	pt_BR
dc.rights	Acesso Aberto	pt_BR
dc.subject	Redes Veiculares	pt_BR
dc.subject	VANET	pt_BR
dc.subject	Verificação probabilística de modelos	pt_BR
dc.subject.other	Vehicular ad hoc network	pt_BR
dc.subject.other	Mobile ad hoc network	pt_BR
dc.subject.other	Probabilistic model checking	pt_BR
dc.subject.other	Computação	pt_BR
dc.title	Verification of vehicular networks using probabilistic model checking	pt_BR
dc.type	Tese de Doutorado	pt_BR
Appears in Collections:	Teses de Doutorado

Files in This Item:

File	Description	Size	Format
brunoferreira.pdf		6.06 MB	Adobe PDF	View/Open

Show simple item record