Verificação de Modelos

Visão geral

A verificação de modelos (model checking) é um método automatizado para verificação formal (formal verification) de se um sistema de estados finitos (finite-state system) satisfaz uma especificação desejada. Em vez de testar alguns cenários, um verificador de modelos explora todos os comportamentos alcançáveis de um modelo do sistema e:

  • Prova que a propriedade vale, ou
  • Refuta a propriedade produzindo um traço de contraexemplo (counterexample trace) (uma execução concreta que viola a propriedade)

A verificação de modelos fica na interseção entre lógica, teoria de autômatos (automata theory) e resolução de restrições (constraint solving). Na prática moderna, ela está fortemente conectada à tecnologia SAT/SMT (ver Resolução de SAT e Satisfatibilidade Módulo Teorias (SMT)).

Domínios de aplicação típicos incluem verificação de hardware, protocolos de comunicação, software concorrente, sistemas embarcados/controladores e, cada vez mais, análises de segurança para componentes usados em sistemas habilitados por IA.

O que é verificado?

Modelo do sistema: sistemas de transição de estados finitos

A maior parte da verificação de modelos começa com um modelo de transição de estados (state-transition model), como uma estrutura de Kripke (Kripke structure):

  • Um conjunto finito de estados (S)
  • Uma relação de transição (transition relation) (R \subseteq S \times S) (possíveis próximos passos)
  • Uma função de rotulagem (L: S \to 2^{AP}) indicando quais proposições atômicas (atomic propositions) são verdadeiras em cada estado (por exemplo, in_critical, error, grant)

Você pode pensar nisso como um grafo direcionado de estados. A verificação de modelos responde a perguntas como:

  • “Um estado de erro é alcançável?”
  • “O sistema sempre evita impasse (deadlock)?”
  • “Se uma requisição acontece, ela é eventualmente atendida?”

Propriedades: segurança vs vivacidade

Muitas propriedades se enquadram em duas classes amplas:

  • Segurança (safety): “coisas ruins nunca acontecem”
    Exemplo: Dois processos nunca estão simultaneamente na seção crítica.
  • Vivacidade (liveness): “coisas boas eventualmente acontecem”
    Exemplo: Toda requisição é eventualmente atendida.

Verificadores de modelos tipicamente aceitam propriedades escritas em lógicas temporais (temporal logics), como LTL e CTL.

Lógicas temporais usadas na verificação de modelos

Lógicas temporais permitem especificar como proposições evoluem ao longo do tempo (ao longo de execuções).

Lógica Temporal Linear (Linear Temporal Logic, LTL)

A Lógica Temporal Linear (LTL) fala sobre um único caminho de execução por vez (tempo linear). Operadores comuns:

  • G φ (“globally”): φ vale em todos os instantes
  • F φ (“finally/eventually”): φ vale em algum instante futuro
  • X φ (“next”): φ vale no próximo estado
  • φ U ψ (“until”): φ vale até que ψ se torne verdadeiro

Exemplo de propriedade de vivacidade:

G (request -> F grant)

Significa: sempre, se request ocorre, então eventualmente grant ocorre mais adiante nessa mesma execução.

Exemplo de propriedade de segurança:

G !(p1_crit & p2_crit)

Significa: nunca é o caso que tanto p1_crit quanto p2_crit sejam verdadeiros.

Lógica da Árvore de Computação (Computation Tree Logic, CTL)

A Lógica da Árvore de Computação (CTL) raciocina sobre futuros ramificados a partir de um estado (uma árvore de computação). Ela combina:

  • Quantificadores de caminho:
    • A: para todos os caminhos
    • E: existe um caminho
  • Operadores temporais (frequentemente G, F, X, U)

Exemplos:

AG !error

Em todos os caminhos, globalmente, error nunca acontece (uma propriedade de segurança).

AG (request -> AF grant)

Em todos os caminhos, sempre que request vale, então em todos os caminhos a partir dali, grant eventualmente acontece (uma propriedade forte de vivacidade/resposta).

EF error

Existe um caminho em que error é eventualmente alcançado (uma consulta de alcançabilidade, muitas vezes usada para depuração).

CTL* e o cálculo-μ (brevemente)

  • CTL* engloba tanto LTL quanto CTL, mas verificá-la costuma ser mais caro.
  • O cálculo-μ modal (modal μ-calculus) expressa muitas propriedades temporais usando pontos fixos mínimos/máximos; é uma base para muitos algoritmos simbólicos.

O problema de verificação de modelos

Dado:

  • Um modelo do sistema (M) (sistema de transição de estados finitos)
  • Uma propriedade (\varphi) (por exemplo, fórmula em LTL/CTL)

Decidir se:

[ M \models \varphi ]

Se não, produzir um contraexemplo (counterexample) — frequentemente uma das saídas mais valiosas na prática, porque fornece uma execução concreta que falha.

Um exemplo prático: segurança de exclusão mútua

Imagine um algoritmo concorrente simples com proposições:

  • p1_crit: processo 1 na seção crítica
  • p2_crit: processo 2 na seção crítica

Um requisito central de segurança:

AG !(p1_crit & p2_crit)

Um verificador de modelos explorará todas as intercalações (interleavings) alcançáveis dos dois processos. Se houver um bug, ele pode retornar um traço de contraexemplo como:

  1. p1_try
  2. p2_try
  3. p1_crit
  4. p2_crit ← violação (ambos verdadeiros)

Isso é muito mais forte do que um teste unitário: demonstra uma intercalação realmente alcançável que viola a especificação.

Abordagens algorítmicas centrais

A verificação de modelos moderna é melhor entendida como uma família de técnicas que diferem em como representam e exploram o espaço de estados.

1) Verificação de modelos de estados explícitos (explicit-state)

Métodos de estados explícitos (explicit-state) representam estados individualmente e os exploram usando algoritmos de grafos (DFS/BFS).

Tarefas comuns:

  • Alcançabilidade (reachability) (encontrar um caminho até error)
  • Detecção de ciclos (cycle detection) (necessária para muitas propriedades de vivacidade)
  • Componentes fortemente conectados (strongly connected components, SCCs) para ciclos de aceitação

Para CTL, a verificação de modelos de estados explícitos frequentemente funciona rotulando estados que satisfazem subfórmulas, usando cálculos de predecessores sobre o grafo.

Para LTL, uma abordagem padrão é a verificação de modelos com base em autômatos (automata-theoretic model checking):

  1. Negar a propriedade: verificar (M \models \varphi) buscando um contraexemplo para (\varphi), isto é, um comportamento que satisfaça (\lnot \varphi).
  2. Traduzir (\lnot \varphi) em um autômato de Büchi (Büchi automaton) (A_{\lnot \varphi}).
  3. Formar o produto (product) do sistema e do autômato: (M \times A_{\lnot \varphi}).
  4. Buscar um ciclo de aceitação (accepting cycle) (uma execução infinita que viola a propriedade).

Se existir um ciclo de aceitação, ele corresponde a um contraexemplo que repete um laço.

Redução por ordem parcial (Partial-Order Reduction, POR)

A concorrência cria números enormes de intercalações. A redução por ordem parcial (Partial-Order Reduction, POR) explora a independência de ações para evitar explorar intercalações equivalentes, preservando a correção para muitas propriedades. Isso é crucial em ferramentas de estados explícitos como o SPIN.

Prós/contras

  • Prós: intuitivo, bons contraexemplos, frequentemente rápido em sistemas “esparsos”
  • Contras: a memória estoura rapidamente (é preciso armazenar estados visitados); tem dificuldade com espaços de estados muito grandes

2) Verificação de modelos simbólica (simbólica) baseada em BDD

Métodos simbólicos (symbolic) representam conjuntos de estados e a relação de transição de forma compacta usando fórmulas Booleanas, classicamente com Diagramas de Decisão Binária (Binary Decision Diagrams, BDDs).

Em vez de “enumerar estados”, a verificação simbólica computa coisas como:

  • Post(S): conjunto de sucessores de um conjunto de estados S
  • Pre(S): conjunto de predecessores

A verificação de CTL se torna uma sequência de cálculos de ponto fixo (fixpoint computations) (pontos fixos mínimos/máximos) sobre essas operações de conjuntos. Por exemplo, alcançabilidade (“EF error”) é um ponto fixo mínimo:

[ Z = error \cup Pre(Z) ]

iterado até convergir.

Por que BDDs podem funcionar (e por que às vezes não)

BDDs podem representar conjuntos enormes de estados de forma compacta quando a estrutura Booleana é favorável (por exemplo, hardware regular). Mas eles também podem explodir exponencialmente com uma ordenação de variáveis (variable ordering) ruim, tornando o desempenho imprevisível.

Prós/contras

  • Prós: pode lidar com espaços de estados extremamente grandes quando os BDDs são compactos; bom para certos projetos de hardware/controle
  • Contras: sensível à ordenação de variáveis; o tamanho dos BDDs pode explodir

3) Verificação de modelos baseada em SAT e verificação de modelos limitada (BMC)

Abordagens baseadas em SAT (SAT-based) reduzem a verificação de modelos à satisfatibilidade proposicional (propositional satisfiability).

Verificação de Modelos Limitada (Bounded Model Checking, BMC)

A verificação de modelos limitada (Bounded Model Checking, BMC) procura contraexemplos de comprimento até um limite (k). Ela:

  1. Codifica o estado inicial (I(s_0))
  2. Codifica a relação de transição por (k) passos: (T(s_0,s_1) \land T(s_1,s_2) \land \cdots \land T(s_{k-1},s_k))
  3. Codifica a negação da propriedade em algum passo (por exemplo, alcançar error até o passo (k))

A fórmula resultante é SAT sse existir um contraexemplo de comprimento ≤ (k).

Uma consulta típica de alcançabilidade via BMC:

I(s0) ∧ T(s0,s1) ∧ ... ∧ T(s(k-1),sk) ∧ (error(s0) ∨ ... ∨ error(sk))

Se for SAT, um resolvedor SAT retorna uma atribuição que pode ser decodificada em um traço de execução.

BMC é amplamente usada porque resolvedores SAT são extremamente otimizados (ver Resolvedores SAT).

Completude e técnicas “não limitadas”

BMC por si só nem sempre é um método de prova: ela pode não encontrar um bug até o limite (k), mas um contraexemplo mais longo pode existir. Para transformar verificação baseada em SAT em técnicas de prova, métodos comuns incluem:

  • k-indução (k-induction): provar invariantes por indução no comprimento do caminho
  • verificação de modelos baseada em interpolação (interpolation-based model checking): generalizar a partir de provas limitadas
  • IC3/PDR (Alcançabilidade Dirigida por Propriedades, Property Directed Reachability): constrói incrementalmente um invariante indutivo usando consultas SAT; altamente eficaz para propriedades de segurança

(Às vezes, esses métodos são agrupados como verificação de modelos não limitada baseada em SAT.)

Prós/contras

  • Prós: excelente para encontrar bugs; se beneficia diretamente do progresso em resolvedores SAT; escala bem para muitos problemas industriais
  • Contras: BMC ingênua é incompleta a menos que seja combinada com métodos de indução/invariantes; escolhas de codificação importam

4) Verificação de modelos baseada em SMT (tipos de dados mais ricos)

Para software e sistemas com aritmética, arrays, vetores de bits ou tipos de dados algébricos, as codificações frequentemente migram de SAT para SMT:

  • SAT é apenas Booleano.
  • SMT adiciona teorias de fundo (aritmética linear, vetores de bits, arrays, funções não interpretadas etc.).

Isso permite verificação limitada/não limitada sem converter tudo (“bit-blastar”) para forma Booleana pura — embora muitas ferramentas ainda dependam de vetores de bits e SAT internamente.

Veja Resolução de SMT e Satisfatibilidade Módulo Teorias (SMT) do lado dos resolvedores.

Complexidade e o problema da explosão de estados

Complexidade teórica (alto nível)

Para um sistema com (n) estados e uma propriedade de tamanho (|\varphi|):

  • A verificação de CTL pode ser feita aproximadamente em tempo (O(n \cdot |\varphi|)), dado acesso explícito ao grafo.
  • A verificação de LTL é PSPACE-completa no tamanho da fórmula e polinomial no tamanho do grafo de estados (mais precisamente, ela é cara em (|\varphi|), e a construção do autômato pode ser exponencial em (|\varphi|)).
  • A verificação de CTL* é ainda mais difícil (EXPTIME-completa).

Na prática, o desafio dominante geralmente não é a complexidade assintótica em (|\varphi|), mas o número de estados alcançáveis.

Explosão de estados

O número de estados globais em um sistema composto se multiplica:

  • Dois componentes com (N) estados cada podem produzir (N^2) estados globais.
  • A concorrência adiciona números enormes de intercalações.

Essa explosão de estados (state explosion) é o principal obstáculo prático na verificação de modelos.

Técnicas comuns de mitigação

  • Representação simbólica (BDDs, codificações SAT/SMT)
  • Redução por ordem parcial (evitar intercalações redundantes)
  • Abstração (abstraction) (superaproximar o sistema)
    • Se o modelo abstrato viola a propriedade, o contraexemplo pode ser espúrio
  • CEGAR (Refinamento de Abstração Guiado por Contraexemplo, Counterexample-Guided Abstraction Refinement): refinar a abstração iterativamente até que o contraexemplo seja real ou a propriedade seja provada
  • Redução por simetria (symmetry reduction) (quociente por permutar componentes idênticos)
  • Raciocínio composicional (compositional reasoning) (verificar componentes com suposições)
  • Redução do cone de influência (cone of influence reduction) (ignorar variáveis irrelevantes para a propriedade)
  • Geração de invariantes (invariant generation) (fortalecer provas; frequentemente via SAT/SMT)

Como a verificação de modelos se conecta a SAT/SMT

Verificação de modelos e resolução de restrições se reforçam mutuamente:

  • BMC baseada em SAT reduz a busca de bugs a SAT.
  • IC3/PDR é essencialmente uma sequência de consultas SAT construindo invariantes indutivos.
  • Verificação de modelos baseada em SMT lida com construções mais próximas de software (inteiros, heaps, arrays).
  • Explosão de bits (bit-blasting) traduz circuitos de vetores de bits para SAT; isso é fundamental na verificação de modelos de hardware.
  • Interpolação de Craig (Craig interpolation) e núcleos UNSAT (UNSAT cores) de SAT/SMT podem ser usados para generalizar provas limitadas em invariantes não limitados.

Se você enxergar SAT/SMT como respondendo “existe uma atribuição que satisfaz restrições?”, então a verificação de modelos frequentemente pergunta “existe uma execução que viola a propriedade?”, e codifica “execução” + “violação” como restrições.

Fluxo de trabalho prático

Um fluxo de trabalho típico de verificação de modelos é:

  1. Modelar o sistema (manualmente, ou extraído de código/HDL)
  2. Especificar a propriedade (LTL/CTL/assertions)
  3. Executar o verificador de modelos
  4. Se houver violação: inspecionar o traço de contraexemplo
  5. Corrigir o projeto ou refinar o modelo/especificação e repetir

Armadilhas comuns de modelagem

  • Suposições sobre o ambiente omitidas (o sistema parece falhar, mas apenas sob entradas impossíveis)
  • Modelos excessivamente abstratos que introduzem comportamentos que o sistema real não pode executar
  • Propriedades incorretas (por exemplo, especificar vivacidade quando apenas segurança é pretendida)
  • Suposições de justiça (fairness assumptions) ausentes (algumas propriedades de vivacidade exigem justiça para excluir comportamentos de “fome do escalonador”)

Ferramentas e ecossistemas (exemplos)

Algumas ferramentas amplamente usadas ilustram estilos diferentes:

  • SPIN: verificação de modelos de estados explícitos para sistemas assíncronos; foco em LTL; forte redução por ordem parcial
  • NuSMV / nuXmv: verificação de modelos simbólica (BDD e baseada em SAT), suporta CTL/LTL e mecanismos avançados
  • CBMC: verificação de modelos limitada para C/C++ (baseada em SAT/SMT)
  • TLC (TLA+): verificação de modelos de estados explícitos de especificações TLA+ (boa para modelagem de sistemas distribuídos)
  • PRISM: verificação de modelos probabilística (cadeias de Markov/MDPs), usada quando a incerteza é explícita

(A verificação de modelos probabilística vai além do não determinismo básico de estados finitos para propriedades quantitativas; é conceitualmente adjacente, mas tipicamente tratada como uma área especializada.)

Verificação de modelos em sistemas adjacentes à IA

Embora a verificação de modelos seja uma técnica clássica de métodos formais, ela aparece cada vez mais em contextos relevantes para IA:

  • Verificação de planejadores e controladores: garantir que um planejador simbólico nunca alcance estados inseguros.
  • Monitoramento em tempo de execução (runtime monitoring): especificações em lógica temporal compiladas em monitores para restrições de segurança.
  • Pilhas de autonomia segura (safe autonomy stacks): verificar a lógica supervisória de estados finitos ao redor de componentes aprendidos.
  • Verificação de políticas para abstrações finitas: aproximar um ambiente contínuo com um modelo de estados finitos e, então, verificar propriedades de alcançabilidade/segurança nessa abstração.

Para modelos aprendidos como redes neurais, a verificação frequentemente usa técnicas diferentes (por exemplo, análise baseada em SMT/MILP de redes lineares por partes), mas o padrão arquitetural é semelhante: especificar propriedades e tentar provar/produzir contraexemplos usando raciocínio automatizado.

Resumo

A verificação de modelos fornece uma forma rigorosa e automatizada de verificar sistemas de estados finitos por meio de:

  • Expressar propriedades de correção em lógicas temporais como LTL e CTL
  • Explorar sistematicamente espaços de estados usando:
    • Busca em grafos de estados explícitos (com reduções como redução por ordem parcial)
    • Cálculo de ponto fixo simbólico (BDDs)
    • Codificações baseadas em SAT/SMT (BMC, k-indução, IC3/PDR)
  • Enfrentar a explosão de estados com abstração, métodos simbólicos e refinamento guiado por resolvedores

Como muitos mecanismos de verificação de modelos são impulsionados por tecnologias SAT/SMT, entender Resolução de SAT e Satisfatibilidade Módulo Teorias (SMT) oferece um caminho prático para entender como ferramentas modernas de verificação escalam.