Modelling and Model-Checking a ROS2 Multi-Robot System using Timed Rebeca

No mundo da robótica, construir uma única máquina que se mova e pense já é difícil o suficiente. Construir uma equipe delas que trabalhe em conjunto sem colidir umas com as outras é um tipo de desafio completamente diferente. Essas máquinas, frequentemente chamadas de robôs móveis autônomos, são projetadas para navegar em ambientes reais, evitando paredes, pessoas e uns aos outros enquanto tentam alcançar destinos específicos. O software que as controla é incrivelmente complexo, dependendo de um fluxo constante de dados de sensores, como lasers, para entender onde estão e o que há ao seu redor. Como esses robôs operam em um mundo físico contínuo, seus movimentos são suaves e fluidos, mudando por frações minúsculas de segundo e milímetros de distância. No entanto, os computadores que os controlam pensam em etapas discretas, processando informações em blocos distintos de tempo. Essa lacuna entre a realidade suave da física e a lógica passo a passo do código cria um ponto cego perigoso. Se o software não estiver perfeitamente ajustado, um robô pode mover-se rápido demais para que seus sensores detectem um obstáculo, ou dois robôs podem chegar à mesma interseção no exato mesmo momento, levando a um impasse onde nenhum consegue se mover.

Para resolver isso, pesquisadores precisam de uma maneira de testar cada cenário possível que uma equipe de robôs possa enfrentar antes mesmo de ligarem as máquinas reais. É aqui que entra um campo chamado verificação formal. Em vez de executar uma simulação algumas vezes e torcer pelo melhor, a verificação formal utiliza a lógica matemática para verificar cada caminho possível que um sistema possa seguir. Ela faz uma pergunta simples, mas poderosa: existe qualquer sequência de eventos, por mais improvável que seja, que cause a falha do sistema? Para uma equipe de robôs, isso significa provar que eles nunca colidirão, nunca ficarão presos para sempre e sempre alcançarão seus objetivos. O desafio sempre foi que os robôs reais se movem em um mundo contínuo, enquanto essas provas matemáticas exigem que o mundo seja dividido em uma grade de etapas fixas. Se as etapas forem muito grandes, a prova perde pequenos, mas críticos, acidentes. Se as etapas forem muito pequenas, o computador fica sobrecarregado pela enorme quantidade de possibilidades e não consegue terminar o cálculo.

Para solucionar isso, um grupo de pesquisadores da Universidade de Mälardalen e da KTH Royal Institute of Technology, na Suécia, desenvolveu uma nova maneira de preencher essa lacuna. Eles criaram um sistema que permite aos engenheiros projetar uma equipe de múltiplos robôs usando uma linguagem de modelagem especializada chamada Timed Rebeca, que trata cada robô como um ator independente que reage a mensagens. Esse modelo é então rigorosamente verificado por um computador para garantir a segurança. Crucialmente, a equipe também escreveu o software real para os robôs usando um sistema padrão chamado ROS2, garantindo que o modelo matemático e o código real estivessem perfeitamente alinhados. Eles não apenas simularam os robôs; eles construíram uma versão do modelo que era abstrata o suficiente para ser verificada por um computador, mas detalhada o suficiente para refletir a física real das máquinas. Ao fazer isso, puderam prever falhas raras e perigosas que as simulações padrão costumam perder.

Os pesquisadores focaram em um cenário envolvendo cinco robôs movendo-se através de uma grade de cinquenta por cinquenta, um espaço aproximadamente do tamanho do chão de um grande armazém. Eles configuraram um ambiente complexo onde os robôs tinham que navegar em torno de obstáculos e cruzar os caminhos uns dos outros para alcançar seus alvos. No mundo real, esses robôs usam scanners a laser para detectar objetos, realizando medições centenas de vezes por segundo. A equipe teve que descobrir como traduzir esses feixes de laser contínuos e movimentos suaves em etapas discretas necessárias para o computador verificar a lógica. Eles descobriram que existe uma relação estrita entre a velocidade com que um robô se move e a frequência com que ele escaneia seus arredores. Se um robô se mover muito rapidamente, ele pode percorrer toda a distância entre dois escaneamentos sem que o sensor perceba um obstáculo em seu caminho. Os pesquisadores provaram que, para o modelo ser preciso, a velocidade do robô precisava ser limitada para que ele não pudesse cruzar uma célula da grade mais rápido do que o tempo necessário para a atualização do sensor. Essa regra, derivada de um princípio fundamental do processamento de sinais, garantiu que o modelo digital não perdesse possíveis colisões.

Para tornar a verificação computacional viável, a equipe teve que simplificar o mundo sem perder a verdade do problema. Eles representaram os robôs não como formas suaves, mas como retângulos movendo-se de uma célula quadrada para outra, girando em incrementos de quarenta e cinco graus. Eles calcularam o tempo necessário para se mover entre essas células com base na velocidade do robô e no tamanho da célula. Eles também pré-calcularam valores trigonométricos complexos, como o seno e o cosseno de ângulos, e os armazenaram em tabelas de consulta (lookup tables) para que o computador não tivesse que calculá-los do zero a cada vez. Essas otimizações permitiram que o verificador de modelos explorasse milhões de estados possíveis em questão de minutos. Quando executavam a verificação, o computador podia dizer com absoluta certeza se um conjunto específico de regras levaria a uma colisão ou a uma chegada segura.

Os resultados de seus experimentos foram impressionantes. Nos casos em que os robôs foram programados com velocidades seguras e tempos de espera variados, o verificador de modelos confirmou que todos os cinco robôs alcançariam seus destinos sem jamais colidirem ou ficarem presos. Os pesquisadores então executaram o código ROS2 real em uma simulação, e os robôs comportaram-se exatamente como o modelo previu, navegando com sucesso pelo espaço lotado. No entanto, quando alteraram os parâmetros para criar uma situação perigosa — como fazer todos os robôs se moverem na mesma velocidade ou definir uma taxa de escaneamento muito baixa para a velocidade — o verificador de modelos encontrou imediatamente uma falha. Ele identificou uma sequência específica de eventos que levaria a uma colisão. Quando executaram o código real com essas mesmas configurações perigosas, a simulação falhou exatamente da mesma forma que o modelo havia previsto. Em um teste, o modelo encontrou uma colisão após explorar apenas alguns milhares de estados, enquanto a simulação real falhou três em cada cinco vezes, confirmando que o perigo era real e previsível.

O estudo também destacou a importância do tempo. Em um cenário, os pesquisadores configuraram os robôs para se moverem a uma velocidade que era apenas ligeiramente rápida demais para a taxa de atualização do sensor. O verificador de modelos descobriu que essa pequena violação da regra de segurança tornava uma colisão quase inevitável, independentemente de como os robôs fossem programados para evitar uns aos outros. O computador mostrou que os robôs chegariam a um ponto de cruzamento ao mesmo tempo e, como não conseguiriam se ver a tempo, colidiriam. A simulação real confirmou isso, com os robôs falhando em evitar uns aos outros em todas as execuções. Isso demonstrou que o modelo não era apenas um exercício teórico, mas uma ferramenta prática capaz de capturar erros sutis e perigosos que os engenheiros humanos poderiam negligenciar.

Os pesquisadores reconheceram que sua abordagem tem limites. O método atual exige que os engenheiros construam manualmente tanto o modelo matemático quanto o código real, o que é um processo demorado que pode introduzir erro humano. Eles também observaram que, embora seu sistema pudesse lidar com cinco robôs em uma grade de cinquenta por cinquenta, escalá-lo para cem robôs ou um mapa muito maior sobrecarregaria rapidamente a memória do computador. O gargalo é o número absoluto de caminhos possíveis que os robôs podem seguir; conforme o número de robôs e o tamanho do mapa aumentam, o número de combinações cresce tão rápido que o computador fica sem espaço para armazená-las. Apesar dessas limitações, o trabalho prova que é possível criar um gêmeo digital de um sistema robótico complexo que seja simples o suficiente para ser verificado e preciso o suficiente para ser confiável.

Esta pesquisa oferece um novo caminho para o desenvolvimento de sistemas autônomos seguros. Ao tratar o design do software de robótica como um processo de construir e verificar um modelo matemático primeiro, os engenheiros podem identificar falhas fatais antes que um único robô seja construído ou implantado. A equipe mostrou que, ao equilibrar cuidadosamente o nível de detalhe no modelo com a necessidade de eficiência computacional, é possível verificar que um sistema de múltiplos robôs se comportará de forma segura no mundo real. Seu trabalho sugere que o futuro da robótica reside não apenas em construir máquinas mais inteligentes, mas em construir melhores maneiras de provar que essas máquinas não falharão quando for mais importante.