Synchronous Observers Revisited for Runtime Verification of Lustre Using STL

Resumo Técnico: Observadores Síncronos Revisitados para Verificação de Tempo de Execução de Lustre Usando STL

Definição do Problema
A Lógica Temporal de Sinais (STL) é uma formalização padrão para especificar propriedades de segurança temporal em sistemas ciber-físicos (CPS), particularmente para verificação de tempo de execução (runtime verification). No entanto, as ferramentas de STL existentes tipicamente operam sobre sinais pré-gravados ou simulados, ou sobre modelos de autômatos abstratos, em vez de operar sobre o código executável que é efetivamente implantado. Consequentemente, há uma carência de uma semântica equivalente de execução em tempo real para propriedades STL aninhadas que rode em sincronia com o sistema monitorado. Além disso, embora linguagens síncronas como Lustre utilizem "observadores síncronos" para verificação estática, o potencial desses observadores para verificação de tempo de execução permanece subexplorado. Um desafio específico reside no tratamento da natureza de "três valores" do monitoramento online: como os operadores temporais limitados olham para o futuro, um monitor não pode sempre decidir uma propriedade imediatamente após um tick, levando a um atraso antes que um veredito definitivo seja alcançado.

Metodologia
Os autores propõem uma técnica para compilar o fragmento síncrono de STL (SSTL) diretamente em observadores síncronos dentro da linguagem de fluxo de dados Lustre. O núcleo da metodologia envolve o "desenrolar" (unrolling) de fórmulas aninhadas em uma coleção finita de obrigações não aninhadas, cada uma monitorando uma janela fixa de ticks de tempo discreto.

1. Semântica de Fluxo de Três Valores: A abordagem adota uma semântica de três valores de Kleene (def_true, def_false, unknown). Em cada tick, o observador emite um veredito baseado no prefixo observado até o momento. Unknown indica que o horizonte da fórmula ainda não transcorreu. Isso é implementado usando um par de sinais Booleanos (pos, neg) representando verdade definitiva e falsidade definitiva, respectivamente.
2. Construção Primitiva (until_leaf): Os autores sintetizam um nó Lustre reutilizável único, until_leaf, que implementa o operador "até" limitado ($U_{[a,b]}$). Este primitivo rastreia uma precondição (o sinal "vivo") e uma pós-condição (o sinal "encontrado") ao longo de uma janela específica. Ele emite def_true ao encontrar uma testemunha e def_false seja via terminação precoce (falha da precondição) ou expiração da janela.
3. Síntese Recursiva: Fórmulas aninhadas são sintetizadas de baixo para cima. O sistema instancia cópias do primitivo until_leaf para cada tick de início exigido pelos operadores externos. Essas cópias são conectadas usando regras de lógica de Kleene para conjunção, disjunção e negação.
   • Para operadores limitados ($\square_{[a,b]}$, $\diamond_{[a,b]}$), a síntese desenrola a fórmula em um conjunto de folhas correspondentes a cada deslocamento inicial dentro do intervalo.
   • Para o operador Global não limitado ($\square$), que é comum em sistemas de execução livre, os autores introduzem uma construção de registrador de deslocamento (shift-register). Em vez de instanciar observadores infinitos, um registrador de tamanho $H+1$ (onde $H$ é o horizonte interno) recicla o estado, permitindo que o monitor rastreie as cópias "vivas" da fórmula interna indefinidamente.
4. Visualização: Uma ferramenta interativa baseada em navegador é fornecida para renderizar os vereditos de três valores de observadores aninhados sobre traços editáveis, auxiliando na depuração e intuição de comportos temporais aninhados complexos.

Principais Contribuições

1. Monitoramento Online Executável: A técnica sintetiza observadores que são compilados junto com o sistema na mesma linguagem síncrona (Lustre), rodando em sincronia com o código executável real, em vez de sobre dados simulados.
2. Aninhamento Arbitrário com Compilação Modular: Ao contrário do trabalho anterior (ex: Bellanger et al.), que era limitado a operadores não aninhados, este método suporta o aninhamento arbitrário de propriedades SSTL limitadas.
3. Operador Externo Não Limitado: A abordagem admite um operador externo globalmente não limitado ($\square$) adequado para monitorar sistemas de execução livre, mantendo a estrutura interna limitada.
4. Utilidade Dupla: Os observadores resultantes servem a um duplo propósito: funcionam como monitores de tempo de execução e, como um subproduto, servem como obrigações de verificação estática para o model checker Kind2, sem a necessidade de um modelo separado.
5. Semântica de Três Valores para Tempo de Execução: A implementação fornece vereditos causais de Kleene, permitindo que os monitores se comprometam com respostas definitivas o mais cedo possível conforme a trilha permitir, muitas vezes antes que o horizonte total da fórmula seja atingido.

Resultados e Avaliação
Os autores avaliaram a técnica em dois estudos de caso: um sistema massa-mola e um cenário de controle de cruzeiro adaptativo (ACC) de carro com frenagem de emergência.

• Corretude: Todos os observadores sintetizados foram verificados contra o model checker Kind2. Os vereditos de tempo de execução e estáticos concordaram em todas as propriedades, incluindo o invariante de exclusão mútua ($pos \land neg = \text{false}$).
• Desempenho: Os observadores foram compilados para C e executados via o interpretador lv6. Os custos de execução por tick foram medidos em nanossegundos (variando de ~6,7 ns a ~206,5 ns dependendo da complexidade), bem abaixo dos períodos de controle típicos de escala de milissegundos, confirmando a viabilidade para implantação online.
• Terminação Precoce: A semântica de três valores provou ser eficaz; nos estudos de caso, as propriedades limitadas estabeleceram vereditos definitivos estritamente antes de seus horizontes teóricos. Por exemplo, uma propriedade profundamente aninhada ($P3$) estabilizou 15 ticks antes.
• Comportamento Não Limitado: O operador $\square$ não limitado funcionou como um mecanismo apenas de falsificação, travando corretamente para def_false quando ocorreram violações (ex: a distância diminuindo abaixo dos limiares de segurança) e permanecendo unknown caso contrário.

Significância e Alegações
O artigo afirma preencher a lacuna entre a especificação formal e o monitoramento de tempo de execução executável para CPS síncronos. Ao sintetizar observadores diretamente na linguagem do sistema, os autores eliminam o "gap de modelagem" frequentemente encontrado ao verificar modelos abstratos contra o código implantado. O trabalho demonstra que propriedades temporais aninhadas complexas podem ser monitoradas online com baixa latência e alta confiabilidade. Os autores posicionam seu trabalho como uma extensão de Bellanger et al. [5], abordindo especificamente as limitações de profundidade de aninhamento e a orientação para verificação apenas estática. A contribuição é apresentada como uma técnica de síntese sistemática que é sonora e completa em relação à semântica explícita de três valores, validada tanto através de execução em tempo real quanto de verificação de modelo estática.

Limitações
Os autores reconhecem três limitações primárias:

1. Explosão de Estados: O número de folhas é o produto das larguras das janelas, o que pode causar o crescimento exponencial do tamanho do observador com intervalos grandes (ex: $\diamond_{[0,100]}$).
2. Suposição de Sistema Fechado: Os estudos de caso modelaram a planta dentro do Lustre como um sistema fechado. Monitorar sistemas abertos genuínos com entradas de sensores externas permanece um passo futuro.
3. Domínio Discreto: A abordagem atual opera estritamente dentro do domínio amostrado e discretizado e ainda não suporta semânticas de robustez de STL contínuo.