Formally Guaranteed Control Adaptation for ODD-Resilient Autonomous Systems

1. O Problema

O desenvolvimento de sistemas autônomos resilientes enfrenta um desafio crítico: garantir desempenho confiável em situações que estão fora do Domínio de Projeto Operacional (ODD - Operational Design Domain).

• Limitações do ODD: O ODD define as condições nas quais um sistema foi projetado para operar com segurança. No entanto, ambientes reais são complexos e dinâmicos, podendo gerar condições não previstas (out-of-ODD).
• Incerteza e Falhas: Quando um sistema encontra condições fora do ODD, seu comportamento torna-se inerentemente incerto. Atualizações de software (redesenho ou re-treinamento) em tempo de execução são frequentemente inviáveis devido a custos ou restrições de tempo.
• Gap na Adaptação: Abordagens existentes de sistemas autônomos adaptativos (SAS) focam na detecção de desvios, mas carecem de um framework para mitigar encontros fora do ODD e adaptar dinamicamente os modelos subjacentes do sistema, mantendo garantias formais de segurança.

2. Metodologia: A Abordagem SAVE

O artigo propõe o SAVE (Situation-Aware Verification and control synthEsis), uma abordagem centrada em situações e orientada pelo ODD. O método divide-se em duas fases principais: Pré-implantação e Implantação (Runtime), operando em um ciclo de adaptação (Monitoramento, Análise, Planejamento, Execução - MAPE-K).

A. Pré-implantação

1. Augmentação da Grade de Cobertura de Situações (SCG):
   • O ODD é usado para gerar um conjunto discreto de situações (tuplas de atributos como densidade de navios, tempo até colisão, etc.).
   • A SCG é estendida com probabilidades de transição derivadas de dados empíricos e testes, criando um modelo probabilístico que inclui estados de falha.
2. Análise de Situações Críticas:
   • São gerados Cadeias de Markov de Tempo Discreto (DTMCs) para cada situação, representando o comportamento do sistema.
   • Utiliza-se Verificação de Modelos Probabilísticos (PMC) com lógica PCTL para verificar propriedades de segurança.
   • Calcula-se uma pontuação de criticidade: quanto maior a violação de uma propriedade de segurança (ex: probabilidade de falha > limite), maior a criticidade. Isso permite priorizar quais situações exigem mitigação antes da implantação.

B. Implantação (Runtime)

O sistema opera em um loop contínuo:

1. Monitoramento (M): O sistema detecta a situação atual ($\rho_t$) e falhas conhecidas.
2. Atualização de Modelo e Análise (A):
   • As probabilidades de transição são atualizadas usando abordagens frequentistas ou bayesianas baseadas nos dados monitorados.
   • Novos modelos DTMC são construídos e analisados via PMC.
   • Se uma violação de segurança for detectada (pontuação de criticidade > 0), o sistema identifica a situação mais crítica.
3. Síntese de Controlador (P):
   • O SAVE sintetiza um novo controlador adaptativo.
   • Mecanismo de Bloqueio: A situação crítica é removida do contexto operacional, transformando seu estado em um "estado sumidouro" (sink state) com probabilidade de transição zero para fora dele. Isso impede fisicamente que o sistema prossiga para aquela condição insegura.
   • O processo é iterativo: após remover uma situação, as pontuações de criticidade de todas as situações restantes são recalculadas. O ciclo continua até que todas as propriedades de segurança sejam satisfeitas ou um limite de iterações seja atingido.
4. Execução (E): O controlador sintetizado e verificado é executado no sistema gerenciado.

3. Principais Contribuições

1. Abordagem Centrada em Situações: Um método que extrai situações do ODD para gerar modelos probabilísticos e sintetizar controladores em tempo de execução, fornecendo garantias quantitativas formais.
2. Métrica de Criticidade e Atualização de Dados: Um método para codificar transições probabilísticas entre situações e uma métrica de pontuação de criticidade que incorpora atualizações baseadas em dados para refinar as probabilidades de transição dinamicamente.
3. Loop de Adaptação Orientado por Verificação: Um mecanismo de runtime que detecta violações de segurança e sintetiza controladores atualizados que permanecem seguros, mesmo sob "deriva" do ODD (ODD drift), bloqueando ativamente situações perigosas.

4. Resultados e Avaliação

A abordagem foi avaliada através de um estudo de caso no domínio marítimo, envolvendo um Navio de Superfície Autônomo Marinho (MASS) navegando entre outros navios.

• Cenário: O sistema deve evitar colisões e manter separação adequada. Foram definidas duas propriedades de segurança (Φ1 e Φ2) relacionadas à probabilidade de falha (colisão iminente ou quase colisão) dentro de 50 passos de tempo.
• Eficácia (RQ1): Em 20 variantes de testes com perturbações fora do ODD (ex: aumento de velocidade dos navios), o SAVE conseguiu evitar violações de requisitos em 14 dos 20 casos. O sistema de base (baseline), sem adaptação, falhou em todos os casos.
• Adaptação (RQ2): O SAVE demonstrou capacidade de reagir a eventos não previstos em tempo real. Ao detectar uma situação de alto risco, o controlador foi adaptado para excluir a situação, prevenindo colisões e restaurando a conformidade com os requisitos de segurança (Φ1 e Φ2) que haviam sido violados no baseline.
• Escalabilidade (RQ3): A análise de tempo de execução mostrou que, embora o número de transições cresça exponencialmente com o número de situações (pior caso), o tempo necessário para gerar pontuações de criticidade permanece viável para sistemas críticos, indicando a viabilidade da verificação em runtime.

5. Significado e Impacto

O trabalho do SAVE representa um avanço significativo na segurança de sistemas autônomos:

• Garantias Formais em Runtime: Diferente de abordagens puramente baseadas em aprendizado de máquina ou testes, o SAVE fornece garantias matemáticas (via PMC) de que o sistema adaptado continuará seguro.
• Resiliência ao ODD: Oferece uma solução prática para o problema de sistemas que encontram condições não previstas, permitindo que continuem operando de forma segura (mesmo que degradada ou restrita) em vez de falhar catastróficamente.
• Rastreabilidade: Estabelece um elo claro entre o ODD de design, dados de teste e verificação em tempo de execução, preenchendo uma lacuna crítica em frameworks de sistemas autônomos adaptativos.

Em resumo, o SAVE demonstra que é possível criar sistemas autônomos que não apenas detectam anomalias, mas que se reconfiguram formalmente para garantir a segurança contínua em ambientes dinâmicos e incertos.