Combining model checking with simulation-based techniques for protocol verification

Resumo Técnico: Combinando Verificação de Modelos com Técnicas Baseadas em Simulação para Verificação de Protocolos

Declaração do Problema
A verificação de modelos é uma técnica rigorosa para verificar sistemas de estados finitos, mas é frequentemente dificultada pelo problema da explosão do espaço de estados. À medida que os parâmetros do sistema aumentam (ex: capacidades de canal ou tamanhos de janela), o espaço de estados alcançável cresce exponencialmente, tornando a verificação exaustiva inviável. Este artigo aborda essa limitação no contexto de protocolos de comunicação, especificamente o Protocolo de Bits Alternados (ABP) e o Protocolo de Janela Deslizante (SWP). Enquanto abstrações mais simples como o Protocolo de Comunicação Simples (SCP) podem ser verificadas diretamente, o aumento dos parâmetros no ABP e no SWP faz com que o espaço de estados exceda as capacidades das ferramentas de verificação de modelos padrão, mesmo com hardware moderno.

Metodologia
Os autores propõem uma metodologia de verificação híbrida que combina verificação de modelos com relações de simulação para superar a explosão do espaço de estados. O fundamento teórico central baseia-se no princípio de que, se uma máquina de estados concreta $M$ é simulada por uma máquina de estados abstrata $M_A$, e $M_A$ satisfaz uma propriedade invariante, então o invariante correspondente se mantém para $M$.

A metodologia é operacionalizada usando a linguagem de lógica de reescrita Maude e envolve dois frameworks primários:

1. Verificação de Simulação Direta:
   Para verificar um protocolo concreto $M$ contra um protocolo abstrato $M_A$:

   • Passo 1: Realizar a verificação de modelo direta na máquina abstrata $M_A$ para verificar sua propriedade invariante.
   • Passo 2: Conjecturar um candidato de relação de simulação $r$ entre $M$ e $M_A$. Provar que o invariante de $M$ é logicamente dedutível do invariante de $M_A$ sob a suposição de $r$, utilizando divisão de casos estática e redução.
   • Passo 3: Demonstrar que $M$ é, de fato, simulado por $M_A$. Isso envolve verificar as condições de simulação (correspondência de estado inicial e preservação de transição) para todas as regras de reescrita de $M$.
   • Implementação: O Passo 3 utiliza um procedimento de três comandos no Maude:
     • srew: Para encontrar estados sucessores em $M$ usando constantes frescas para representar valores arbitrários.
     • red: Para verificar se a relação de simulação se mantém entre os estados concretos e abstratos.
     • search: Para confirmar que a máquina abstrata pode alcançar um estado correspondente em zero ou mais passos.
   • Para garantir a correção apesar do uso de supersetos de estados alcançáveis (devido à indecidibilidade do alcance), os autores empregam o Lema 1, que prova que verificar a condição de transição sobre esses supersetos é suficiente para garantir a condição sobre os estados realmente alcançáveis.

2. Composição de Relações de Simulação:
   Para sistemas altamente complexos onde uma única abstração é insuficiente, os autores propõem uma abordagem hierárquica. Isso envolve o encadeamento de relações de simulação (ex: $SWP \to ABP \to SCP$).

   • O invariante do sistema mais concreto é deduzido do sistema intermediário, que por sua vez é deduzido do sistema mais abstrato.
   • Isso permite a verificação de sistemas com espaços de estados massivos, aproveitando os invariantes verificados de abstrações mais simples e em camadas.

Principais Contribuições
O artigo apresenta duas contribuições principais:

1. Uma metodologia que combina verificação de modelos com relações de simulação para verificar sistemas onde a verificação de modelos direta falha devido à explosão do espaço de estados.
2. Uma metodologia para a composição de relações de simulação, permitindo a verificação hierárquica ao vincular múltiplas camadas de abstração para lidar com modelos ainda maiores e mais complexos.

Resultados e Estudos de Caso
Os autores avaliaram sua abordagem usando três protocolos: SCP, ABP e SWP.

• Estudo de Caso I (ABP):

  • Desafio: A verificação de modelo direta do ABP com maxIndex = 64 e maxQueueLength = 32 resultou em um tempo limite (timeout > 3.600 segundos) devido à explosão do espaço de estados.
  • Solução: Os autores estabeleceram uma relação de simulação do ABP para o mais simples SCP.
  • Resultado: Todo o processo de verificação (verificação do SCP, dedução do invariante e verificação da simulação) foi concluído em menos de 1 segundo por etapa. Isso confirmou que o ABP satisfaz sua propriedade invariante sem a exploração exaustiva de estados.

• Estudo de Caso II (SWP):

  • Desafio: O SWP introduz gerenciamento de janela e números de sequência, criando um espaço de estados significativamente maior que o do ABP, tornando a verificação direta impossível.
  • Solução: Os autores empregaram a composição de relações de simulação: $SWP \to ABP \to SCP$. Eles verificaram a simulação de SWP para ABP e combinaram-na com a relação previamente verificada de ABP para SCP.
  • Resultado: A abordagem hierárquica verificou com sucesso a propriedade invariante do SWP (garantindo que as mensagens sejam recebidas em ordem, sem perda ou duplicação) com parâmetros (windowSize = 16, maxQueueLength = 32) que seriam inviáveis para a verificação direta.

Significância e Alegações
O artigo alega que esta abordagem mitiga efetivamente o problema da explosão do espaço de estados, deslocando o fardo computacional da travessia exaustiva de estados para a verificação simbólica em modelos menores e abstratos. Aspectos-chave da significância incluem:

• Escalabilidade: O método permite a verificação formal de protocolos com grandes parâmetros (ex: tamanhos de janela e comprimentos de fila) que estão além do alcance da verificação de modelos direta.
• Reutilização: Especificações formais existentes podem ser reutilizadas como modelos abstratos para novos alvos mais complexos, reduzindo significativamente o esforço de verificação.
• Automação e Rigor: Embora a construção dos modelos abstratos e das relações de simulação exija conhecimento de domínio manual, a validade dessas relações é verificada de forma semi-automática usando comandos padrão do Maude. Os autores desenvolveram uma ferramenta de suporte para automatizar a divisão de casos e a execução de comandos, minimizando o erro humano.
• Distinção de Trabalhos Existentes: Diferente da Refinação de Abstração Guiada por Contraexemplos (CEGAR), que é reativa e refina modelos com base em contraexemplos espúrios, esta abordagem é proativa, aproveitando o conhecimento de domínio para construir abstrações estratégicas. Isso proporciona maior transparência e interpretabilidade, pois as relações de simulação mantêm um mapeamento compreensível para humanos entre os comportamentos concretos e abstratos.

Os autores concluem que, ao operacionalizar a teoria da simulação em uma sequência padronizada de comandos Maude, eles preencheram a lacuna entre as relações teóricas abstratas e os fluxos de trabalho de verificação executáveis, oferecendo um caminho prático e eficiente para a verificação de sistemas distribuídos complexos.