💬 NLP

ESBMC-PLC: Formal Verification of IEC 61131-3 Ladder Diagram Programs Using SMT-Based Model Checking

Este artigo apresenta o ESBMC-PLC, o primeiro verificador formal de código aberto que suporta nativamente programas de Diagrama de Escada (Ladder Diagram) da norma IEC 61131-3 ao traduzi-los em uma representação intermediária para verificação de modelos baseada em SMT, verificando com sucesso propriedades de segurança e detectando bugs em diversos benchmarks industriais, ao mesmo tempo em que aborda lacunas de pesquisa fundamentais na área.

Autores originais: Pierre Dantas, Lucas Cordeiro, Waldir Junior

Publicado 2026-06-16

📖 5 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Pierre Dantas, Lucas Cordeiro, Waldir Junior

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine uma fábrica onde máquinas gigantes, misturadores químicos e sinais de trem são controlados por um cérebro minúsculo e incansável chamado PLC (Controlador Lógico Programável). Essas máquinas funcionam com base em um tipo especial de manual de instruções chamado Diagrama de Escada (Ladder Diagram). Pense nisso como o desenho de uma escada onde cada "degrau" é uma regra: "Se a luz vermelha estiver acesa E o botão for pressionado, então ligue o motor".

Por décadas, engenheiros escreveram essas regras desenhando-as, não digitando código. Isso tornou muito difícil para os "inspetores de segurança" modernos (ferramentas de verificação formal) checarem se as regras eram perfeitas, porque os inspetores só entendiam código digitado, não desenhos.

Este artigo apresenta o ESBMC-PLC, uma nova ferramenta que atua como um tradutor universal e um inspetor de segurança super rigoroso, tudo em um só.

Veja como ele funciona, usando analogias simples:

1. O Tradutor (A "Pedra de Roseta")

Antes desta ferramenta, você não conseguia pedir a um computador para verificar um desenho. O ESBMC-PLC pega o "Diagrama de Escada" gráfico (o desenho) e o traduz instantaneamente para uma linguagem que o computador entende (um código intermediário baseado em texto).

A Analogia: Imagine que você tem uma receita escrita em um caderno de esboços com desenhos dos ingredientes. O ESBC-PLC é o chef que olha para as imagens e escreve instantaneamente as instruções exatas em texto: "Adicione 2 xícaras de farinha, depois mexa". Agora, o computador pode ler a receita.

2. O Simulador (O "Loop de Viagem no Tempo")

Um PLC não roda apenas uma vez; ele roda em um loop, verificando sensores e alterando saídas milhares de vezes por segundo.

A Analogia: A maioria das verificações de segurança olha para um único momento no tempo. O ESBMC-PLC é como um simulador de viagem no tempo que executa o "dia" da fábrica repetidamente. Mas, em vez de apenas reproduzir um dia específico, ele simula todos os dias possíveis de uma só vez. Ele pergunta: "E se o sensor quebrar? E se o botão for pressionado duas vezes? E se a energia oscilar?" Ele verifica todas as combinações de eventos para ver se um desastre pode acontecer.

3. A Prova "Ilimitada" (A "Garantia de Para Sempre")

As ferramentas antigas só podiam verificar um número limitado de etapas (como verificar os primeiros 100 dias de vida de uma fábrica). Se um erro acontecesse no dia 101, elas o perderiam.

A Analogia: O ESBMC-PLC usa um truque matemático especial chamado k-indução. Em vez de contar os dias um por um, ele prova uma regra que diz: "Se a fábrica estiver segura hoje, e as regras forem seguidas, ela estará segura amanhã, no dia seguinte e para sempre". Ele oferece uma garantia de para sempre de que a máquina nunca irá falhar, desde que as regras sejam seguidas.

4. A Linguagem "Sem Lógica" (O "Checklist em Linguagem Comum")

Normalmente, para pedir a um computador que verificasse a segurança, era necessário conhecer lógica matemática complexa (lógica temporal).

A Analogia: O ESBMC-PLC permite que os engenheiros escrevam regras de segurança em um simples checklist YAML (como uma lista de tarefas).
- Em vez de: "Para todo tempo t, se A é verdadeiro, então B deve ser falso."
- Você escreve: "O motor e o interruptor de reversão nunca devem estar ligados ao mesmo tempo."
  A ferramenta entende essa linguagem comum e verifica isso automaticamente.

O Que Eles Descobriram?

Os autores testaram esta ferramenta em 13 programas de fábrica diferentes, variando de controles de motores simples a semáforos complexos e bombas de água. Eles usaram programas de fornecedores do mundo real (como CONTROLLINO e MathWorks) que não foram projetados para serem testados, apenas para ver se a ferramenta conseguiria lidar com eles.

Os Resultados:
- 100% de Precisão: Identificou corretamente todos os programas seguros e todos os programas inseguros.
- Encontrou Bugs Ocultos: Encontrou 8 bugs específicos que os testes padrão não detectaram. Por exemplo, encontrou um cenário onde um botão de parada de emergência desligava a máquina, mas falhava em resetar um temporizador, fazendo com que a máquina reiniciasse imediatamente quando o botão fosse solto.
- Velocidade: Verificou todos esses programas em menos de 60 milissegundos (mais rápido que um piscar de olhos humano).

A Conclusão

Este artigo apresenta a primeira ferramenta de código aberto que pode pegar um desenho industrial padrão (Diagrama de Escada), traduzi-lo e provar matematicamente que ele é seguro para sempre. Ela preenche a lacuna entre a forma gráfica tradicional que os engenheiros usam para projetar máquinas e a forma matemática de alta tecnologia que os computadores usam para verificar a segurança.

Nota Importante: O artigo afirma que isso funciona para as partes "principais" da programação industrial (lógica booleana, temporizadores, contadores). Ele ainda não lida com recursos complexos como números de ponto flutuante ou matrizes de dados avançadas, mas para a grande maioria da lógica de segurança crítica, ele funciona perfeitamente e está pronto para uso hoje.

Resumo Técnico: ESBMC-PLC

Declaração do Problema

Controladores Lógicos Programáveis (PLCs) são críticos para a segurança industrial, mas a notação de programação dominante, o Diagrama de Escada (LD) padronizado na IEC 61131-3, permanece amplamente ausente do ecossistema de verificação formal. Ferramentas de modelagem baseadas em Satisfatibilidade de Teoria de Modos (SMT), como o ESBMC, amadureceram para softwares de propósito geral (C, Rust, Python), mas não conseguem processar diretamente a notação gráfica de "degraus e bobinas" (rung-and-coil) do LD. As soluções existentes ou exigem tradução manual para linguagens textuais (introduzindo riscos de fidelidade), ou dependem de ferramentas proprietárias, ou carecem de suporte para provas de segurança ilimitadas. Consequentemente, a lógica de segurança crítica industrial escapa da verificação matemática rigorosa disponível para outros domínios de software, deixando sistemas vulneráveis a defeitos de projeto e injeções de código malicioso, como as Bombas de Lógica de Escada (Ladder Logic Bombs - LLB).

Metodologia

O artigo apresenta o ESBMC-PLC, um verificador formal de código aberto implementado como um novo frontend para o Efficient SMT-based Context-Bounded Model Checker (ESBMC). A metodologia centra-se num pipeline de tradução direta de PLCopen XML (o formato de intercâmbio aberto para LD) para o GOTO-Intermediate Representation (IR) interno do ESBMC.

Arquitetura Central

Parsing de Entrada: A ferramenta aceita arquivos PLCopen XML (formatos textuais e gráficos tc6_0201) exportados pelos principais fabricantes (Siemens, Rockwell, CODESYS, OpenPLC). Ela reconstrói a topologia do circuito a partir de IDs de referência sem necessidade de edição manual.
Tradução para GOTO-IR:
- Modelagem do Ciclo de Varredura (Scan Cycle): O modelo de execução do PLC é codificado como um loop while(true).
- Gestão de Estado: As variáveis de entrada são reamostradas de forma não determinística a cada iteração (modelando um ambiente de sensores de mundo aberto). As bobinas de saída e marcadores internos são modelados como variáveis estáticas persistentes, preservando o estado entre os ciclos de varredura.
- Mapeamento de Elementos: Elementos de LD (contatos XIC/XIO, bobinas OTE/OTL/OTU, temporizadores TON/TOF/TP, contadores CTU/CTD) são traduzidos em operações GOTO-IR. As regras de tradução são projetadas para corresponder às semânticas formais definidas por Ebnenasir [9], particularmente em relação à prioridade de retenção (latch priority - OTL/OTU) e contadores acionados por borda.
- Tipos de Dados: Tipos IEC 61131-3 são mapeados para seus equivalentes em C mais reduzidos (ex: BOOL para bool, TIME para uint32_t representando milissegundos).
Especificação de Propriedades: Uma linguagem baseada em YAML permite que engenheiros especifiquem cinco tipos de propriedades de segurança sem necessidade de conhecimento em lógica temporal: mutual_exclusion (exclusão mútua), invariant (invariante), absence (ausência), response (resposta) e reachability (alcançabilidade).
Mecanismo de Verificação: O backend utiliza o ESBMC com o solver SMT Z3. Ele suporta:
- BMC Incremental: Para a rápida detecção de bugs em programas inseguros.
- k-Indução: Para provas de segurança ilimitadas, verificando propriedades para todos os possíveis ciclos de varredura sem a necessidade de unrolling manual de loops.

Principais Contribuições

Primeiro Frontend Nativo de LD de Código Aberto: O ESBMC-PLC é a primeira ferramenta de código aberto a aceitar nativamente programas LD em formato PLCopen XML padrão, eliminando a necessidade de tradução manual para C ou ST.
Provas Ilimitadas para LD: É a primeira ferramenta a aplicar k-indução a programas LD, permitindo provas de segurança ilimitadas em vez de depender apenas de modelagem de verificação limitada (bounded model checking).
Contraexemplos Acionáveis: A ferramenta gera contraexemplos referenciando os nomes originais das variáveis de LD, tornando-os diretamente interpretáveis por engenheiros de automação.
Análise Sistemática de Lacunas: Um levantamento de 22 estudos (2020–2026) identificou quatro lacunas de pesquisa; o ESBMC-PLC aborda diretamente a falta de um tradutor de LD para formal de código aberto e a ausência de um frontend ESBMC para IEC 61131-3.
Suíte de Benchmarks: Os autores introduziram uma suíte de 13 benchmarks abrangendo seis domínios industriais e três fontes (originais, sintéticos e programas de fornecedores do mundo real), incluindo programas não modificados da CONTROLLINO e MathWorks.

Resultados Experimentais

A avaliação foi conduzida em 13 benchmarks (7 seguros, 6 inseguros) em seis domínios industriais (motores, transporte, segurança, infraestrutura, indústria alimentícia, edifícios).

Precisão de Classificação: O ESBMC-PLC classificou corretamente todos os 13 benchmarks com zero falsos positivos e zero falsos negativos. Isso incluiu 4 programas de fornecedores independentes (Categoria C) que não foram pré-rotulados pelos autores.
Detecção de Bugs: A ferramenta identificou 8 bugs distintos através das variantes inseguras. Estes incluíram:
- Falha ao resetar temporizadores após parada de emergência (CS2).
- Lógica de reset sobrepondo sinais de desligamento de emergência (CS3).
- Falta de intertravamentos para ativação simultânea de fases em semáforos (CS4).
- Condições de corrida onde sinais de porta aberta eram ativados no mesmo ciclo de varredura que o início do motor (CS8).
- Ativação simultânea de bombas e válvulas sob condições de falha de sensor (CS12).
Desempenho: Todas as 61 verificações de propriedades foram concluídas em menos de 60 ms em Apple Silicon (aarch64).
Provas Ilimitadas: Todos os 7 programas seguros foram verificados usando k-indução (convergindo em $k=2$ ), fornecendo garantias de segurança incondicionais.
Validação no Mundo Real: A ferramenta processou e verificou com sucesso programas reais do repositório CONTROLLINO e da documentação do MathWorks Simulink PLC Coder sem pré-processamento.

Significância e Alegações

O artigo afirma que o ESBMC-PLC demonstra que a verificação formal de Ladder Logic de PLCs industriais é uma operação prática, de código aberto e de sub-segundo, acessível a engenheiros de automação.

Posicionamento Único: Ao contrário do estado da arte PLCverif (que depende de CBMC e requer entrada em ST/SCL), o ESBMC-PLC é a única ferramenta de código aberto que combina entrada LD nativa, provas ilimitadas via k-indução e semântica de bit-vector SMT.
Impacto Prático: Ao detectar bugs que os testes funcionais convencionais perdem (como cenários de falha de sensor e condições de corrida dependentes da ordem do ciclo de varredura), a ferramenta aborda lacunas críticas de segurança em sistemas de controle industrial.
Limitações e Escopo: Os autores observam modestamente que as regras de tradução são validadas empiricamente contra as semânticas de Ebnenasir, mas não são formalmente provadas como equivalentes ao padrão IEC 61131-3. A implementação atual cobre um subconjunto central de construtos (excluindo REAL/FLOAT, strings, arrays e programas multi-POU) e ainda não suporta extensões específicas de fornecedores, como tarefas de interrupção.

O artigo conclui que o ESBMC-PLC fecha lacunas de pesquisa significativas e sugere que uma plataforma unificada integrando o frontend LD do ESBMC-PLC com o pipeline ST do PLCverif representa uma direção futura lógica para a verificação de nível industrial.