Use este identificador para citar ou linkar para este item:
http://repositorio.utfpr.edu.br/jspui/handle/1/15905
Título: | Implementação e verificação formal de planos de um agente racional modelado para condução de um veículo autônomo |
Título(s) alternativo(s): | Implementation and formal verification of plans of a rational agent modeled to control an autonomous vehicle |
Autor(es): | Fernandes, Lucas Emanuel Ramos |
Orientador(es): | Alves, Gleifer Vaz |
Palavras-chave: | Sistemas inteligentes de veículos rodoviários Desenvolvimento orientado para o trânsito Computação Intelligent transportation systems Transit-oriented development Computer science |
Data do documento: | 9-Jun-2017 |
Editor: | Universidade Tecnológica Federal do Paraná |
Câmpus: | Ponta Grossa |
Citação: | FERNANDES, Lucas Emanuel Ramos. Implementação e verificação formal de planos de um agente racional modelado para condução de um veículo autônomo. 2017. 200 f. Trabalho de Conclusão de Curso (Graduação) - Universidade Tecnológica Federal do Paraná, Ponta Grossa, 2017. |
Resumo: | Em um futuro não tão distante, veículos autônomos serão uma realidade no tráfego urbano. Atualmente, pesquisas estão sendo realizadas para desenvolver essa nova tecnologia. Isto visa a criação de um sistema capaz de tomar suas próprias decisões sem intervenção humana no controle de um veículo. Neste trabalho é abordado o uso de um agente racional para modelar o comportamento de um veículo autônomo, considerando um mecanismo de condução básica. No cenário aqui considerado, este agente é capaz de atender corridas, transitar em um ambiente simulado, realizar desvio de obstáculos estáticos e conhecidos, e em caso de uma colisão inevitável, o agente tenta minimizar o dano (físico) causado ao veículo quando possível. A implementação do agente capaz de realizar autonomamente tais funções é feita por meio da linguagem Gwendolen. O ambiente onde o agente está inserido, desenvolvido em Java, é responsável por armazenar informações sobre todas as posições nas quais o veículo possa vir a se movimentar. Com o objetivo de obter uma representação gráfica das modificações ocorridas no ambiente, foi criado um simulador independente capaz de se comunicar com o ambiente Java pela rede. Como todo software é susceptível a erros, faz se necessário verificar as decisões tomadas pelo agente. Isto é evidenciado neste cenário, pois falhas no sistema comando um veículo autônomo pode causar fatalidades. Essa validação pode ser feita por meio de técnicas de verificação formal; onde é utilizado fórmulas lógica de linguagem temporal para especificar formalmente as propriedades que são esperadas do agente e, a técnica do model checking program para verifica-las. Com o auxílio da ferramenta AJPF (Agent Java PathFinder), é possível realizar a verificação durante o tempo de execução do agente, assim podendo se garantir a veracidade de uma propriedade durante seu funcionamento e, em casos onde há inconsistência em uma propriedade, dados relevantes para a investigação são fornecidos. Desta forma, aqui é proposto uma implementação de um agente racional e a verificação formal da tomada de decisão, onde tal agente representa um veículo autônomo operando em diferentes cenários simulados. Por meio deste trabalho, foi concluído que é possível realizar o desenvolvimento de um agente na linguagem Gwendolen modelado como um veículo autônomo. Além disso, as propriedades de tal agente podem ser verificadas formalmente através do model checker, utilizando a ferramenta AJPF. |
Abstract: | Autonomous vehicles, in the not too distant future, will be a reality in urban traffic. Currently, various research is being conducted to develop this new technology. The main goal of said research is to create and implement vehicle systems capable, and without human interaction, of making their own decisions. In this work, we will discuss the use of a rational agent to model the behavior of an autonomous vehicle, where a basic driving mechanism is considered. The scenario presented here is to define the following agent abilities: perform rides, move through a simulated environment, obstacle avoidance of static and known barriers, and given a situation when a collision is unavoidable; the agent will try to assure the least amount of (physical) damage to the vehicle possible. The approach taken to create this agent is with the Gwendolen programming language. Once formed, it will be implemented in a Java developed environment. The Java environment is then responsible for storing all information about locations were the agent may move during its performance. Once complete, the use of a UPD protocol will be implemented to receive messages through a local network from the Java environment. This is to create a graphical representation of when changes occur caused by the agent in the said environment. Since all software is prone to errors, it is necessary to verify the decisions taken by the agent. Evidence of such a need is easily understood through the basic knowledge of human impact, specifically human casualties. If a decisional flaw occurs in the system while controlling an autonomous vehicle it could directly impact human life. Such validation, shall be shown, can be performed with formal verification techniques. For this, linear temporal logic formulae is used to formally specify all the properties expected for the agent to hold. The Model Checking Program Technique with AJPF (Agent Java Pathfinder) then makes the verification possible. The latter is a tool which is used to verify agent properties during its run-time. Its purpose is to guarantee that a property hold and show true data to an investigation of an occurring error. Thus, this work proposes an implementation of a rational agent and the formal verification of its decision-making process, where such agent represent an autonomous vehicle in different simulated scenarios. With this work, it is was concluded that it is possible to develop an agent in the Gwendolen language modeled as an autonomous vehicle. In addition to this, the properties of such agent can be formally verified through the model checker using the AJPF tool. |
URI: | http://repositorio.utfpr.edu.br/jspui/handle/1/15905 |
Aparece nas coleções: | PG - Ciência da Computação |
Arquivos associados a este item:
Arquivo | Descrição | Tamanho | Formato | |
---|---|---|---|---|
PG_COCIC_2017_1_08.pdf | 11,43 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.