Comparing Autonomous Vacuum Cleaners Based on Coverage Path
Planning of Grid-based Maps with Model-Checking
Robôs de limpeza autônomos. Verificação de Modelos. Verificação Formal. Mapas baseados em grid. Avaliação de Algoritmos
A integração da verificação formal com validação empírica é crucial para garantir a corretude e eficiência de sistemas robótico autônomos. Este trabalho apresenta uma metodologia inovadora para avaliar o desempenho de robôs de limpeza autônomos utilizando a álgebra de processos Communicating Sequential Processes e o sistema educacional RoboMind para exploração e validação da sua combinação. O Estudo estabelece a garantia de corretude para planejamento de caminhos por cobertura utilizando Communicating Sequential Processes (CSP), enquanto RoboMind serve como um ambiente de teste controlado para validar a navegação em diferentes ambientes. A principal contribuição deste estudo é o desenvolvimento de uma modelagem formalizada que permite uma avaliação sistemática e quantitativa de quatro algoritmos de robô de limpeza, considerando eficiência de cobertura e custo computacional. A abordagem envolve o uso de CSP como linguagem formal para definir o comportamento dos algoritmos de limpeza e do RoboMind como ferramenta de simulação para sua execução e análise. Um estudo de caso é apresentado, aplicando essa estratégia para comparar quatro algoritmos distintos de robôs de limpeza. Os resultados demonstram a eficácia da abordagem proposta, provendo uma forte garantia de corretude enquanto aprimora a aplicabilidade na simulação. Além disso, esta pesquisa destaca o potencial da combinação de CSP e RoboMind para investigações no domínio dos sistemas autônomos.