Implementação, simulação e verificação formal de um agente racional condutor de um veículo autônomo

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.