Resumo Técnico: Um Framework Unificado para Verificação em Tempo de Execução e Diagnóstico Baseado em Modelo em Lola

Declaração do Problema

Sistemas críticos de segurança exigem não apenas a detecção de falhas, mas também a localização de suas causas raízes para permitir uma mitigação eficaz. Enquanto a Verificação em Tempo de Execução (Runtime Verification - RV) é eficaz para detectar desvios do comportamento especificado durante a execução, e o Diagnóstico Baseado em Modelo (Model-Based Diagnosis - MBD) é um framework principista para identificar componentes defeituosos, essas duas técnicas operam historicamente de forma isolada. Os monitores de RV tradicionais analisam o comportamento do sistema sobre sequências de estados potencialmente ilimitadas para detectar violações, ao passo que o MBD tipicamente opera em um único ponto no tempo, não especificado, após uma falha ter sido detectada. Além disso, as integrações existentes frequentemente falham em mapear ações de falha detectadas diretamente para componentes anormais no sentido do MBD ou carecem de capacidade para lidar com entradas incertas e dinâmicas de falhas temporais dentro de um framework de raciocínio baseado em fluxos (streams) unificado.

Metodologia

O artigo propõe um framework unificado que integra RV baseada em fluxos e MBD dentro da Lola, uma linguagem de especificação baseada em fluxos síncronos. A metodologia central envolve a codificação de informações de verificação e diagnóstico como fluxos especializados, permitindo observação contínua e raciocínio simbólico sob incerteza.

1. Codificação Unificada em Lola

Os autores mapeiam um sistema diagnosticado $S = (sd, comps)$ para um Sistema Lola $(\phi, comps)$:

• Descrição do Sistema ($sd$): Codificada no fluxo de suposições ($\alpha$), que é verdadeiro por definição. Este fluxo contém o conhecimento comportamental (ex: $\neg ab(c) \to beh_c$) e o conhecimento geral do sistema.
• Componentes ($comps$): Cada componente $c$ é representado por um fluxo Booleano interno onde true indica que o componente está anormal ($ab(c)$).
• Observações: Variáveis observáveis do sistema (entradas/saídas) são modeladas como fluxos de entrada, que podem ser certos (determinísticos) ou incertos (intervalos ou conjuntos não-determinísticos).
• Variáveis Não Observáveis: Valores internos do sistema não medidos diretamente são modelados como fluxos internos.
• Instância de Problema de Diagnóstico (DPI): Uma tupla $(\phi, comps, \Psi)$, onde $\Psi$ representa o histórico de restrições de entrada até o tempo atual.

2. Raciocínio Simbólico e Computação de Diagnóstico

O framework utiliza um monitor simbólico que mantém um conjunto de restrições $[\phi]_{\Psi}^{\leq t}$ representando todos os comportamentos possíveis do sistema consistentes com as observações até o tempo $t$.

• Resolução de Restrições: Um solver SMT (ex: Z3) é usado para verificar a consistência e derivar implicações.
• Derivação de Diagnóstico: Um diagnóstico é uma suposição sobre o estado (normal/anormal) dos componentes que torna a descrição do sistema consistente com as observações. O framework computa diagnósticos mínimos identificando conflitos mínimos (conjuntos de componentes que não podem ser todos normais) e calculando seus conjuntos de cobertura mínima (minimal hitting sets).
• Poda (Pruning): Para garantir monitoramento de tempo constante e espaço constante, estratégias de poda reescrevem as restrições para limitar o tamanho do conjunto de restrições, retendo apenas a informação histórica necessária.

3. Cenários de Diagnóstico

O framework suporta três modos distintos de diagnóstico baseados na natureza temporal das falhas dos componentes:

• Diagnóstico Multi-Instante: Assume que os estados dos componentes são estáticos sobre uma janela de $k$ instantes passados ($t-k$ até $t$). Um diagnóstico de $k$-instantes explica todas as observações dentro desta janela. O artigo prova que, para especificações atemporais, diagnósticos de $k$-instantes são equivalentes à agregação de diagnósticos de instante único, mas para especificações temporais (com offsets não nulos), eles fornecem resultados mais focados.
• Diagnóstico Temporal: Permite que os estados dos componentes mudem ao longo do tempo. Um diagnóstico $k$-temporal é um conjunto de pares $(c, t')$ indicando que o componente $c$ é anormal especificamente no tempo $t'$. Isso é crítico para identificar falhas transitórias (ex: superaquecimento) ou falhas que se manifestam posteriormente devido à propagação.
• Configurações Estendidas: O framework incorpora naturalmente conhecimento de fundo (forçando componentes a serem normais), modelos de falha fortes (especificando comportamentos defeituosos específicos) e modelagem abstrata.

Contribuições Principais

1. Codificação Unificada: Um método para expressar descrições de sistema e suposições de diagnóstico como fluxos especializados em Lola, representando implicitamente todos os diagnósticos válidos para o comportamento observado.
2. Teoria de Diagnóstico Multi-Instante: Uma teoria generalizada para diagnosticar falhas invariantes no tempo sobre uma janela de observação deslizante, que subsume o diagnóstico de múltiplas observações padrão como um caso especial.
3. Diagnóstico Temporal: Suporte para anormalidade variante no tempo, permitindo a identificação de quando uma falha ocorre, não apenas qual componente está defeituoso.
4. Cenários de Diagnóstico Flexíveis: A capacidade de lidar elegantemente com conhecimento de fundo, modelagem abstrata e vários tipos de falhas (persistentes vs. transitórias) dentro de um único framework baseado em fluxos.
5. Implementação e Avaliação: Uma implementação prototípica integrando o algoritmo HS-Tree, QuickXplain e Z3, validada nos benchmarks ISCAS85 e ISCAS89.

Resultados

Os autores avaliaram o framework em dois circuitos Booleanos:

• c17 (ISCAS85): Um circuito puramente combinacional com 6 componentes.
• s27 (ISCAS89): Um circuito sequencial com 14 componentes.

Descobertas:

• Viabilidade: O framework identificou com sucesso falhas reais injetadas (stuck-at-false) em ambos os circuitos.
• Precisão Temporal: Para o circuito sequencial (s27), o framework localizou corretamente as falhas apenas quando a janela de observação ($k$) era grande o suficiente para cobrir a origem da falha e o tempo de propagação.
• Desempenho:
  • O tempo de execução aumentou com valores maiores de $k$. Para o c17, o diagnóstico de $k$-instante levou até 246 ms ($k=0$) e 775 ms ($k=31$) por instante.
  • O diagnóstico temporal foi significativamente mais caro devido à explosão combinatória de tratar $(c, t')$ como componentes distintos. Para o c17, o diagnóstico temporal levou até 8,7 segundos por instante para $k=5$ e 136 segundos para $k=12$.
  • Apesar do custo computacional, os autores observam que, com $k$ constante, os tempos de execução permaneceram independentes do comprimento total do traço, confirmando a viabilidade das estratégias de poda.

Significância e Alegações

O artigo alega fornecer uma integração compacta e bem fundamentada de Verificação em Tempo de Execução e Diagnóstico Baseado em Modelo. Sua significância reside em preencher a lacavra entre a detecção automática de falhas (RV) e a localização sistemática de causas raízes (MBD) dentro de um único framework baseado em fluxos.

Os autores enfatizam que esta abordagem:

• Suporta entradas incertas e suposições ambientais, permitindo inferência refinada baseada em conhecimento especializado.
• Permite o diagnóstico online ao alavancar o raciocínio simbólico para produzir vereditos em cada ponto temporal.
• Oferece uma combinação sinérgica onde os pontos fortes da RV (monitoramento eficiente e contínuo) e do MBD (análise de causa raiz principista) são unificados.
• Fornece um framework robusto (sound) onde o monitor simbólico garante que os valores deduzidos sejam consistentes com todos os mundos possíveis definidos pelas restrições.

O trabalho é apresentado como uma prova de conceito que demonstra a viabilidade do uso da Lola para tarefas de diagnóstico complexas, oferecendo uma base teórica para futuras aplicações práticas em sistemas críticos de segurança.