💻 computer science

Predictive Varanus: Combining CSP Conformance Monitoring with Predictive LTL Runtime Verification

Este artigo introduz o Predictive Varanus, um pipeline de verificação em tempo de execução de dois estágios que combina o monitoramento de conformidade baseado em CSP com a análise preditiva de LTL para permitir a detecção precoce de violações de segurança em sistemas autônomos ao aproveitar modelos de tempo de projeto existentes.

Autores originais: Angelo Ferrando, Matt Luckcuck, Pedro Ribeiro

Publicado 2026-09-17

📖 5 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Angelo Ferrando, Matt Luckcuck, Pedro Ribeiro

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Robôs autônomos, desde os rovers que exploram Marte até os drones que entregam encomendas, operam em um mundo que nunca é totalmente previsível. Mesmo a máquina mais cuidadosamente projetada pode encontrar uma falha de sensor, um obstáculo inesperado ou uma situação que os engenheiros jamais imaginaram. Para manter esses sistemas seguros, cientistas utilizam uma técnica chamada verificação em tempo de execução (runtime verification). Pense nisso como um copiloto vigilante que observa cada movimento do robô em tempo real, checando suas ações contra um conjunto de regras escritas antes da missão começar. Se o robô tentar fazer algo proibido, o copiloto soa um alarme. No entanto, essa abordagem tradicional possui uma falha crítica: ela é reativa. Ela só levanta o alarme depois que o evento ruim já aconteceu. Em ambientes de alto risco, como uma instalação nuclear ou uma missão no espaço profundo, esperar que um erro ocorra para só então reagir pode ser tarde demais. O objetivo dos pesquisadores é construir um sistema que não apenas observe erros, mas que os antecipe, prevendo uma falha antes mesmo de o robô dar o primeiro passo em direção a ela.

Este é o desafio enfrentado por uma equipe de pesquisadores que desenvolveu um novo sistema de monitoramento chamado Predictive Varanus. O sistema foi projetado para robôs autônomos, sendo testado especificamente em um rover simulado encarregado de inspecionar um depósito de resíduos nucleares. Os pesquisadores combinaram duas tecnologias existentes para criar um pipeline que é ao mesmo tempo rigoroso sobre o que o robô tem permissão para fazer e inteligente o suficiente para prever o que acontecerá a seguir. A primeira parte do sistema atua como um porteiro. Ela utiliza um mapa detalhado do comportamento pretendido do robô, escrito em uma linguagem formal chamada Processos Sequenciais Comunicantes (Communicating Sequential Processes), para verificar cada evento realizado pelo robô. Se o robô tentar se mover para um local que não deveria visitar, ou ignorar um comando de segurança, o porteiro rejeita imediatamente essa ação como inválida. Isso garante que o robô permaneça dentro dos limites de seu projeto.

A segunda parte do sistema é onde ocorre a previsão. Uma vez que o porteiro confirma que as ações atuais do robô são válidas, o sistema olha para frente. Ele faz uma pergunta simples, porém poderosa: dado que o robô está se comportando corretamente agora, quais são os únicos futuros possíveis que ele pode seguir? Ao analisar os caminhos restantes permitidos pelo mapa de design do robô, o sistema pode determinar se um resultado específico é agora inevitável. Ele não adivinha possibilidades aleatórias; ele considera apenas os futuros que são consistentes com as próprias regras do robô. Se o robô encontrou um nível de radiação elevado, o sistema sabe que o único caminho futuro permitido é retornar e abortar a missão. Portanto, mesmo antes de o robô realmente retornar, o sistema pode prever com certeza que a missão falhará. Da mesma forma, se o robô visitou com sucesso todos os seus pontos de controle obrigatórios, o sistema pode prever que a missão terá sucesso, mesmo que o robô ainda tenha alguns movimentos a fazer antes de parar oficialmente.

Os pesquisadores testaram essa abordagem em seu rover de inspeção nuclear, que foi programado para visitar cinco diferentes pontos de passagem e verificar níveis de radiação. Os níveis foram categorizados como verde, laranja ou vermelho. Se o rover visse laranja ou vermelho, as regras ditavam que ele deveria retornar ao início e abortar. No monitoramento padrão, o sistema só saberia que a missão estava condenada após o rover realmente retornar. Com o Predictive Varanus, o sistema pôde declarar a missão como uma falha dois eventos antes de o rover sequer iniciar sua jornada de retorno. Em outros cenários, ele pôde prever uma conclusão bem-sucedida oito eventos antes de o robô terminar sua tarefa final. Esse alerta precoce oferece aos operadores humanos ou ao próprio software de controle do robô um tempo valioso para reagir, talvez replanejando uma rota ou preparando um desligamento seguro, em vez de simplesmente observar o desenrolar de uma falha.

O estudo também mediu quanta capacidade de processamento esse nível extra de pensamento exigia. A parte do porteiro permaneceu muito rápida, levando menos de um milissegundo por evento, mesmo conforme o mapa de comportamento do robô crescia. A parte preditiva, que realiza o trabalho pesado de olhar para frente, levou mais tempo, especialmente à medida que os comportamentos possíveis do robô tornavam-se mais complexos. Para um modelo com 200 estados diferentes, a verificação preditiva levou cerca de 700 milissegundos por evento. Embora seja mais lento, os pesquisadores descobriram que o benefício de saber o resultado antecipadamente valia o custo em muitas situações. O sistema identificou com sucesso falhas inevitáveis e sucessos inevitáveis em cenários onde o robô ainda estava seguindo as regras, provando que é possível olhar para o futuro sem quebrar as leis do presente.

O que torna este trabalho significativo não é apenas o fato de ele prever o futuro, mas sim como o faz. Ele não depende de um modelo separado e abstrato para a previsão. Em vez disso, ele reutiliza o exato mesmo mapa de design que foi usado para verificar o comportamento do robô inicialmente. Isso significa que o sistema não está fazendo suposições sobre como o robô pode se comportar; ele está seguindo estritamente a lógica que os engenheiros já construíram na máquina. Os pesquisadores mostraram que, ao combinar uma verificação rigorosa de validade atual com uma verificação prospectiva de inevitabilidade futura, eles poderiam fornecer vereditos mais precoces e úteis do que o monitoramento padrão. O sistema não prevê falhas aleatórias ou problemas de sensores que nunca foram modelados; ele prevê as consequências lógicas do próprio design do robô. No mundo complexo e incerto da robótica autônoma, essa capacidade de enxergar o resultado inevitável de um caminho correto oferece um novo tipo de segurança, transformando um alarme reativo em um guia proativo.

Resumo Técnico: Predictive Varanus

Definição do Problema
A Verificação de Tempo de Execução (Runtime Verification - RV) é uma técnica crítica para sistemas autônomos e robóticos, oferecendo garantia online ao verificar traços de execução observados contra especificações formais sem a necessidade de acesso ao código-fonte ou estados internos. No entanto, a RV padrão é inerentemente reativa; ela só pode detectar violações após um evento indesejado já ter ocorrido. Em domínios de segurança crítica onde falhas são custosas, essa latência é insuficiente. Embora a Verificação de Tempo de Execução Preditiva (Predictive Runtime Verification - PRV) aborde isso analisando possíveis continuações futuras para determinar a satisfação ou violação inevitável de propriedades, as abordagens existentes frequentemente dependem de modelos que são distintos das especificações de tempo de projeto do sistema. Além disso, a PRV padrão não distingue inerentemente entre um sistema que se comporta de acordo com seu modelo, mas viola uma propriedade temporal, versus um sistema que se comporta de uma maneira inteiramente não modelada (fora da especificação).

Metodologia
O artigo apresenta o PREDICTIVE VARANUS, um pipeline de verificação de dois estágios que integra a ferramenta existente VARANUS com a Verificação de Tempo de Execução Preditiva para Lógica Temporal de Tempo Linear (LTL). A inovação central é o reuso de um único modelo de Processos Sequenciais Comunicantes (CSP) de tempo de projeto tanto para a verificação de conformidade quanto para o raciocínio preditivo.

O pipeline opera da seguinte forma:

Portão de Conformidade CSP (VARANUS): O sistema sob análise (SUA) emite um traço de eventos. O primeiro estágio utiliza um modelo CSP como um oráculo determinístico. O VARANUS verifica se o traço atual é um prefixo válido da linguagem do modelo CSP. Se um evento não for permitido pelo modelo, o traço é imediatamente rejeitado (rej). Isso garante que o raciocínio preditivo seja aplicado apenas ao comportamento que é consistente com o design do sistema.
Tradução do Modelo: Para traços que passam pelo portão de conformidade, o modelo CSP é traduzido em um autômato de Büchi (no formato Hanoi Omega-Automata). Esta tradução envolve:
- Extração do Sistema de Transição Rotulado (LTS) do processo CSP.
- Mapeamento de eventos CSP para proposições atômicas.
- Adição de auto-loops skip a estados terminais para converter traços finitos em palavras infinitas, habilitando a semântica padrão de LTL.
Monitoramento LTL Preditivo: O monitor preditivo utiliza o autômato de Büchi traduzido para restringir o conjunto de futuros admissíveis. Dada uma propriedade LTL $\phi$ $ϕ$ , o monitor computa os produtos síncronos do autômato derivado do CSP com os autômatos para $\phi$ $ϕ$ e $\neg\phi$ $\neg ϕ$ .
- Se todas as continuações consistentes com o modelo satisfazem $\phi$ , o veredito é satisfação conclusiva ( $\top$ ).
- Se todas as continuações consistentes com o modelo violam $\phi$ , o veredito é violação conclusiva ( $\bot$ ).
- Se ambos os resultados permanecem possíveis, o veredito é inconclusivo ( $?$ ).
- Se o traço foi rejeitado pelo VARANUS, o veredito é rej.

Principais Contribuições

Pipeline Integrado: O artigo define um pipeline formal de dois estágios que combina o monitoramento de conformidade baseado em CSP com a verificação preditiva de LTL.
Reuso de Modelo: Demonstra como um único modelo CSP, tipicamente usado para análise de tempo de projeto (ex: com FDR ou RoboChart), pode servir a propósitos duplos: como um oráculo de tempo de execução para conformidade e como a fonte de futuros admissíveis para predição.
Semântica Formal: Os autores fornecem definições formais para a função de veredito combinada, distinguindo entre rej (não conformidade com o modelo) e $\bot$ preditivo (violação inevitável dentro do modelo).
Implementação e Tradução: O trabalho detalha a construção do $\omega$ -autômato proposicional a partir de processos CSP, permitindo o uso de ferramentas LTL padrão (como o Spot) enquanto preserva as restrições estruturais do modelo CSP.

Resultos
A abordagem foi avaliada utilizando um estudo de caso de um rover robótico para inspeção de depósitos nucleares e testes de estresse sintéticos.

Estudo de Caso do Rover: O sistema monitorou propriedades relativas à conclusão da missão, cobertura e condições de aborto.
- Em cenários onde radiação perigosa foi detectada, o sistema previu a falha da missão (violação de conclusão/cobertura) e a inevitabilidade de um aborto de 1 a 2 eventos antes do evento de aborto real ocorrer no traço.
- Para missões nominais, a propriedade de cobertura foi prevista como satisfeita 8 eventos antes do evento de conclusão da missão.
- Traços inválidos (ex: continuar após um perigo) foram rejeitados imediatamente pelo VARANUS, sem ganho preditivo, confirmando que o sistema lida corretamente com comportamentos fora do modelo.
- O overhead de tempo de execução foi modesto para o rover (aprox. 1,84 ms/evento no total), com a verificação CSP levando 0,19 ms e o monitor preditivo 1,64 ms.
Testes de Estresse Sintéticos:
- Escalabilidade: A verificação de conformidade CSP permaneceu leve (<1 ms/evento) mesmo conforme o tamanho do modelo aumentava. No entanto, o custo do monitor preditivo escalou significativamente com o tamanho do modelo (de ~0,2 ms/evento para 10 estados a ~700 ms/evento para 200 estados), identificando a construção e manutenção de autômatos como o principal gargalo.
- Ganho de Antecipação: Em benchmarks de decisão de cauda (decision-tail), o ganho de antecipação (o número de eventos economizados pela predição) cresceu linearmente com o comprimento da cauda forçada após um ponto de compromisso. Para um comprimento de cauda de 20, o sistema forneceu um veredito 21 eventos antes de um monitor reativo.

Significância e Alegações
O artigo alega que o PREDICTIVE VARANUS oferece um método prático para alcançar vereditos mais precoces em verificação de tempo de execução ao alavancar modelos CSP existentes de tempo de projeto. Sua significância reside em:

Diferenciação de Modos de Falha: Ele separa claramente o comportamento "fora do modelo" (detectado pelo VARANUS) da "violação inevitável de propriedade" dentro do modelo (detectada pela PRV).
Utilidade Operacional: O estudo de caso demonstra que vereditos preditivos podem ser gerados cedo o suficiente para serem úteis para operadores humanos ou algoritmos de replanejamento, especificamente ao identificar abortos de missão ou falhas inevitáveis antes que elas se manifestem fisicamente.
Modularidade: O pipeline é modular; embora a implementação atual utilize LTL, a estrutura permite que outras técnicas de raciocínio preditivo sejam integradas sem alterar a camada de conformidade CSP.

Os autores reconhecem que a implementação atual enfrenta desafios de escalabilidade em relação ao componente preditivo para modelos grandes, sugerindo que trabalhos futuros possam focar na otimização do backend de autômatos ou na exploração de representações simbólicas. Eles não alegam resolver o problema geral de prever falhas físicas não modeladas, mas sim antecipar resultados que são forçados pelo próprio modelo de design do sistema.

Mais como este