TREBL -- A Relative Complete Temporal Event-B Logic. Part I: Theory

1. O Problema

A verificação de condições de vivacidade (liveness) em métodos formais baseados em estados, como Event-B, TLA+ e Máquinas de Estado Abstrato (ASMs), é um desafio significativo.

• Limitação da Expressividade: As lógicas temporais clássicas (LTL, CTL) são proposicionais e, portanto, têm expressividade limitada quando aplicadas a sistemas complexos que requerem quantificação sobre variáveis de estado.
• Limitação da Completude: Extensões de primeira ordem das lógicas temporais ganham expressividade, mas perdem a completude (não é possível derivar todas as fórmulas válidas).
• Interpretação sobre Traços vs. Estados: A maioria das abordagens anteriores interpreta fórmulas temporais sobre traços (sequências de estados). Isso dificulta a integração com métodos baseados em estados, onde um estado inicial determina todos os traços possíveis a partir dele. Além disso, trabalhos anteriores (como [FRS+24]) exigiam restrições fortes (como "tail-homogeneidade") para provar a completude relativa, limitando a aplicabilidade prática.

O objetivo central é criar uma lógica temporal para Event-B que seja expressiva o suficiente para capturar propriedades de traços complexos, mas que mantenha a completude relativa (garantindo que, se uma propriedade é válida, existe uma prova derivável) e interprete fórmulas sobre estados, não sobre traços.

2. Metodologia

Os autores propõem uma extensão da lógica do Event-B chamada TREBL (Temporal Event-B Logic). A metodologia baseia-se nos seguintes pilares:

• Interpretação sobre Estados: Em vez de interpretar fórmulas temporais sobre sequências infinitas de estados (traços), a lógica é construída de modo que todas as fórmulas sejam interpretadas sobre o estado inicial de um traço. Isso é possível porque, no Event-B, um estado determina completamente o conjunto de traços que dele partem.
• Extensão da Lógica (Lext): Os autores introduzem uma extensão da lógica do Event-B ($L_{ext}$) que inclui:
  • Conjuntos de Atualização (Update Sets): Para representar explicitamente as transições de estado (o efeito de disparar um evento).
  • Operadores Modais de Atualização: Fórmulas da forma $[X]\phi$, significando "após aplicar o conjunto de atualização $X$, a propriedade $\phi$ é verdadeira".
  • Composição de Passos: Definição indutiva de conjuntos de atualização para múltiplos passos ($USet^*(k, X)$), permitindo raciocinar sobre sequências de estados sem sair do domínio da lógica de primeira ordem com conjuntos.
• Operadores Temporais como Atalhos: Os operadores temporais clássicos (ALWAYS $\square$, EVENTUALLY $\diamond$, UNTIL $U$) e suas variações (para um único traço ou subconjuntos de traços) são definidos como "atalhos" (shortcuts) para fórmulas complexas em $L_{ext}$.
• Variantes e Refinamento: Para provar a completude relativa, o sistema utiliza termos de variante (variant terms) que mapeiam estados para conjuntos bem-fundados (como números naturais). O artigo prova que, para qualquer máquina Event-B que satisfaça uma propriedade de vivacidade, é sempre possível realizar um refinamento conservador da máquina para incluir os termos de variante necessários para a prova.

3. Principais Contribuições

1. Definição de TREBL: A definição formal de um fragmento da lógica temporal do Event-B capaz de expressar invariantes, existência, progresso, persistência e alcançabilidade, tanto para todos os traços quanto para traços específicos ou subconjuntos definíveis de traços.
2. Regras de Derivação Sonoras: Apresentação de um conjunto completo de regras de derivação para provar propriedades de vivacidade. Estas regras generalizam trabalhos anteriores (Hoang & Abrial, Ferrarotti et al.) e incluem:
   • Regras para Invariância (INV).
   • Regras para Existência e Persistência usando variantes de convergência ($c$-variant), divergência ($d$-variant) e variantes locais ($lc$, $ld$).
   • Regras para Progresso usando variantes simultâneas e variantes condicionais, eliminando a necessidade de suposições de tail-homogeneidade.
3. Prova de Completude Relativa: Demonstração teórica de que o sistema de derivação é relativamente completo. Isso significa que, para qualquer fórmula válida em uma máquina Event-B suficientemente refinada (onde os termos de variante necessários são definíveis), existe uma derivação formal.
4. Remoção de Restrições: Diferente de trabalhos anteriores, esta abordagem remove a restrição de "tail-homogeneidade", permitindo a verificação de sistemas com não-determinismo intrínseco mais complexo.
5. Aplicação em Segurança: Demonstração da utilidade da lógica através de exemplos de segurança, como não-interferência (non-interference) e dedutibilidade limitada (bounded deducibility), mostrando que propriedades complexas de segurança podem ser expressas como invariantes de transição simples no TREBL.

4. Resultados

• Correção (Soundness): Foi provado que todas as regras de derivação propostas são sonoras; ou seja, se uma fórmula é derivável, ela é semanticamente válida para a máquina.
• Completude Relativa: Foi provado que, sob a premissa de que a máquina foi refinada para conter os termos de variante necessários, toda fórmula válida é derivável.
• Existência de Refinamentos: O artigo prova que refinamentos conservadores que introduzem os termos de variante necessários (como contadores de passos ou cópias de variáveis de estado) sempre existem. Isso garante que a completude relativa não é apenas teórica, mas alcançável na prática através de refinamento.
• Exemplos Práticos: A lógica foi aplicada com sucesso em exemplos de um sistema produtor-consumidor e em modelos de segurança (pilhas com múltiplos níveis de acesso), demonstrando que condições de vivacidade e segurança complexas podem ser verificadas mecanicamente.

5. Significância

O trabalho representa um avanço significativo na verificação formal de sistemas baseados em estados:

• Ponte entre Lógica Temporal e Baseada em Estados: Resolve o dilema entre expressividade e completude ao interpretar fórmulas temporais sobre estados, alinhando-se perfeitamente com a filosofia do Event-B e métodos similares.
• Viabilidade de Verificação Automática: Ao estabelecer a completude relativa e a existência de refinamentos para variantes, o trabalho valida a possibilidade de ferramentas automáticas (como o RODIN, mencionado para a Parte II do artigo) verificarem propriedades de vivacidade complexas sem intervenção manual excessiva, desde que o refinamento adequado seja feito.
• Generalidade: Embora focado no Event-B, a abordagem é generalizável para outros métodos baseados em estados (como ASMs e TLA+), sugerindo uma nova direção para a lógica temporal em métodos formais rigorosos.
• Impacto na Segurança: A capacidade de expressar não-interferência e outras propriedades de segurança como invariantes de transição dentro de uma lógica temporal completa oferece novas ferramentas poderosas para a análise de sistemas críticos e seguros.

Em resumo, o TREBL fornece uma base teórica robusta e praticamente aplicável para a verificação de propriedades de vivacidade em sistemas formais, superando limitações de expressividade e completude de abordagens anteriores.