Synchronous Signal Temporal Logic for Decidable Verification of Cyber-Physical Systems

1. O Problema

Os Sistemas Ciber-Físicos (CPS), como veículos autônomos, robôs agrícolas e dispositivos médicos (ex.: marcapassos), operam em ambientes críticos onde a segurança e a confiabilidade são essenciais. A Lógica Temporal de Sinais (STL - Signal Temporal Logic) é amplamente utilizada para especificar propriedades temporais sobre sinais contínuos nesses sistemas.

No entanto, o artigo identifica um obstáculo fundamental: a verificação estática de propriedades STL é indecidível em geral. Isso ocorre porque os sinais físicos são contínuos (tempo real), e verificar se uma propriedade é satisfeita exigiria avaliar infinitos pontos em um intervalo contínuo. Embora métodos de verificação em tempo de execução (runtime) existam, eles não garantem a segurança antes da implantação e não cobrem todas as trajetórias possíveis. Além disso, a verificação de propriedades de vivacidade (liveness - "algo bom eventualmente acontece") em STL para sistemas autônomos nunca foi realizada de forma estática e decidível.

2. Metodologia: SSTL e a Hipótese de Invariância de Sinal

Os autores propõem a Lógica Temporal de Sinais Síncrona (SSTL - Synchronous Signal Temporal Logic), um fragmento decidível da STL projetado para sistemas que operam em tempo discreto. A metodologia baseia-se nos seguintes pilares:

• Discretização do Tempo: O tempo contínuo ($t \in \mathbb{R}_{\ge 0}$) é projetado para tempo discreto ($[t] \in \mathbb{N}_{\ge 0}$) através de um período de amostragem fixo ($\Delta t$), chamado de "ticks".
• Hipótese de Invariância de Sinal (SIH - Signal Invariance Hypothesis): Esta é a contribuição teórica central. A SIH assume que o valor de um sinal permanece invariante (constante) entre dois ticks consecutivos. Formalmente, para qualquer $t$ dentro de um intervalo de tick $[k\Delta t, (k+1)\Delta t)$, o valor do sinal não muda.
  • Justificativa: Baseia-se na inércia de sinais físicos e no princípio de Nyquist. Se a taxa de amostragem for suficientemente alta, a representação por etapas (piecewise-constant) não perde informações críticas entre as amostras.
• Equivalência Teórica: Os autores provam que, sob a SIH, a satisfação de uma fórmula STL no tempo contínuo é equivalente à satisfação de sua contraparte SSTL no tempo discreto. Isso transforma um problema indecidível em um decidível.
• Tradução para LTLP (LTL com Predicados): Para permitir a verificação automatizada, as fórmulas SSTL são traduzidas para LTLP (Linear Temporal Logic com Predicados).
  • Os operadores temporais com limites de tempo (ex.: "dentro de $[a, b]$") são mapeados para predicados aritméticos sobre índices de estado ($j$) e contadores de obrigação ($j_0$).
  • A tradução lida com aninhamento de operadores e intervalos de tempo acoplados.

3. Contribuições Principais

1. Definição da SSTL: Introdução da primeira abstração síncrona (discreta) da lógica STL, com sintaxe e semântica formais.
2. Prova de Decidibilidade: Demonstração de que a verificação de SSTL é decidível e completa sob a SIH, permitindo a verificação estática tanto de propriedades de segurança (nada de ruim acontece) quanto de vivacidade (algo bom acontece eventualmente).
3. Mecanismo de Tradução: Desenvolvimento de um algoritmo de tradução recursiva de SSTL para LTLP, permitindo o uso de verificadores de modelo padrão (como o SPIN).
4. Validação em Modelos Complexos: Aplicação e verificação bem-sucedida em um modelo cardíaco humano de 33 nós, demonstrando a capacidade de lidar com dinâmicas fisiológicas complexas e restrições de tempo precisas.

4. Resultados e Avaliação

Os autores avaliaram a abordagem em três estudos de caso com complexidade crescente, utilizando o verificador de modelo SPIN:

• Controlador de Semáforo: Um sistema discreto simples. A SSTL verificou corretamente propriedades de segurança (exclusão mútua) e vivacidade. Uma propriedade de "justiça" falhou, indicando um erro no modelo ou especificação, o que demonstra a eficácia da ferramenta em detectar falhas.
• Passagem de Pedestres: Um sistema com sinais de valor inteiro (tamanho de fila). A SSTL verificou com sucesso restrições de segurança e limites de fila. Propriedades de resposta com limites de tempo falharam, novamente apontando para falhas no modelo, com tempos de verificação variando de segundos a minutos.
• Modelo Cardíaco (33 nós): O caso mais complexo, simulando a condução elétrica do coração.
  • Coração Saudável: Todas as propriedades de segurança (condução atrioventricular, período refratário) e vivacidade foram verificadas como satisfeitas.
  • Coração Doente: Ao introduzir bloqueios de condução (AV, LBB, RBB), a propriedade de condução AV ($\varphi_{AV}$) falhou, enquanto as propriedades de vivacidade permaneceram satisfeitas. Isso confirmou que a ferramenta consegue distinguir entre falhas de timing e falhas de liveness.
  • Desempenho: Os tempos de verificação variaram de ~6s a ~66s para o modelo cardíaco. O uso de memória foi alto (até 9GB) devido à discretização de sinais de ponto flutuante para inteiros, mas foi viável.

5. Significado e Impacto

O trabalho é significativo porque:

• Resolve a Indecidibilidade: Oferece uma via prática para a verificação estática de sistemas ciber-físicos contínuos, algo que antes era considerado impossível para propriedades gerais de STL.
• Abordagem Híbrida: Combina a precisão da lógica temporal contínua com a eficiência da verificação de modelos discretos.
• Aplicabilidade em Saúde e Autonomia: A validação em um modelo cardíaco realista abre caminho para o uso de verificação formal no desenvolvimento de dispositivos médicos implantáveis e sistemas autônomos críticos, garantindo que restrições de tempo fisiológicas sejam rigorosamente atendidas.
• Ferramental Prático: Ao traduzir para LTLP e usar o SPIN, a metodologia torna-se acessível a engenheiros que já utilizam ferramentas de verificação de modelo padrão, sem a necessidade de desenvolver novos motores de verificação do zero.

Em resumo, a SSTL fornece uma base teórica e prática sólida para garantir a segurança e a vivacidade de sistemas ciber-físicos complexos através de verificação estática decidível, superando as limitações da lógica temporal contínua tradicional.