Use este identificador para citar ou linkar para este item: http://repositorio.roca.utfpr.edu.br/jspui/handle/1/9734
Título: Implementação, simulação e verificação formal de um agente racional condutor de um veículo autônomo
Título(s) alternativo(s): Implementation, simulation and formal verification of a rational agent as a driver on an autonomous vehicle
Autor(es): Abade, Carlos Eduardo
Alonzo, Priscilla Dorado Gaertner
Orientador(es): Ranthum, Geraldo
Palavras-chave: Veículos a motor
Detectores
Métodos de simulação
Motor vehicles
Detectors
Simulation methods
Data do documento: 20-Jun-2018
Editor: Universidade Tecnológica Federal do Paraná
Câmpus: Ponta Grossa
Referência: ABADE, Carlos Eduardo; ALONZO, Priscilla Dorado Gaertner. Implementação, simulação e verificação formal de um agente racional condutor de um veículo autônomo. 2018. 128 f. Trabalho de Conclusão de Curso (Ciência da Computação) - Universidade Tecnológica Federal do Paraná, Ponta Grossa, 2018.
Resumo: Tecnologias autônomas vem sendo implementadas para aumentar a segurança nos veículos. As reduções no número de fatalidades devido a essas tecnologias abrem novas oportunidades para melhoria do tráfego urbano. Veículos autônomos serão uma realidade em um futuro não muito distante auxiliando nessa melhoria e gerando novos modelos de mobilidade, pois são capazes de serem controlado sem intervenção humana. O controlador de um veículo autônomo cuida de vários elementos no qual a condução está inclusa. Apesar de ser uma tecnologia promissora, testes onde o controlador assumia a condução total do veículo causaram acidentes levando ao cancelamento temporário de alguns projetos na área. Para que os veículos autônomos possam realmente ajudar na melhoria do tráfego e diminuir a quantidade de acidentes no trânsito é preciso garantir que seu funcionamento está correto, de acordo com a implementação do controlador, e buscar mapear e solucionar cenários críticos não pensados durante a programação do sistema. Para isso técnicas de simulação e verificação formal são utilizadas gerando novos conhecimentos sobre esta tecnologia e corrigindo erros que, em testes urbanos, seriam fatais. Neste trabalho um agente racional é modelado como condutor de um veículo autônomo em um ambiente onde deverá realizar ações quanto ao desvio de obstáculos, obedecer a regra de não ultrapassar um semáforo no estado vermelho e aguardar a travessia de um pedestre na faixa de pedestres. Para isso a implementação foi feita com uso da linguagem Gwendolen para agentes racionais. O ambiente, desenvolvido em Java, é simulado a fim de reconhecer as escolhas do agente durante sua rota. O simulador utilizado é uma melhoria de um sistema desenvolvido para a simulação específica de um ambiente em Gwendolen. A linguagem Gwendolen é utilizada porque permite verificar formalmente o comportamento de um determinado agente usando o framework MCAPL. Em um trabalho anterior, um agente racional foi implementado e formalmente verificado usando o algoritmo MCAPL, Gwendolen e Java. Neste trabalho foi desenvolvido um novo ambiente simulado buscando modelar o comportamento de um agente em um ambiente mais próximo de um tráfego urbano real usando pistas, semáforos e pedestres. Como resultado, este trabalho mostra que é possível modelar, implementar e verificar formalmente um agente racional como condutor de um veículo autônomo usando o framework MCAPL, Gwendolen e Java.
Abstract: Autonomous technology has been implemented to increase the vehicles’ safety. The reduction in the numbers of fatalities due to these technologies opens new opportunities for improvement of the urban traffic. Autonomous vehicles will be a reality soon, aiding in this improvement and generating new movability models, since it is able to be controlled without no human intervention. The autonomous vehicle’s controller takes care of several elements which the conduction is included. Despite of being a promising technology, tests where the controller assumed the total conduction of the vehicle caused accidents leading to temporary cancelling of some projects in the area. In order to autonomous vehicle could really help in the improvement of the traffic and diminish the quantity of accidents in the transit, it is needed to assure that its operation is correct according to the implementation of the controller, and seek to map and solve critical scenarios unthought during the system’s programming. For that, simulation techniques and formal verification are used, creating new knowledge about this technology and checking errors that, in urban tests, would be fatal. In this work, a rational agent is modeled as an autonomous vehicle’s driver in an environment where it should perform actions related to obstacles’ detour, obey the rule of not go over the traffic light when the same is red, and wait the crossing of some pedestrian on the crosswalk. For this, the implementation was made through the language Gwendolen for rational agents. The environment, developed in Java, is simulated in order to acknowledge the agent’s choices during its route. The used simulator is an improvement of a system developed to the specific simulation of an environment in Gwendolen. We have used Gwendolen because it allows one to formal verify the behaviour of a given agent using MCAPL framework. On a previous work a rational agent has been implemented and formal verified using algo MCAPL, Gwendolen and Java. Here we have create a new simulated environment trying to model the behaviour of an agent in an environment closer to a real urban traffic by using lanes, traffic lights, and pedestrians. As a result, our work shows that it is possible to model, implement and formal verify a rational agent as a driver on an autonomous vehicle using MCAPL framework, Gwendolen and Java.
URI: http://repositorio.roca.utfpr.edu.br/jspui/handle/1/9734
Aparece nas coleções:PG - Ciência da Computação

Arquivos associados a este item:
Arquivo Descrição TamanhoFormato 
PG_COCIC_2018_1_03.pdf8,3 MBAdobe PDFVisualizar/Abrir


Os itens no repositório estão protegidos por copyright, com todos os direitos reservados, salvo quando é indicado o contrário.