ESBMC‑PLC · Projeto INOVA CETELI/UFAM
A lógica do CLP falha em silêncio. Nós achamos o defeito antes da linha parar.
Verificação formal aplicada a programas Ladder (IEC 61131-3). Provamos matematicamente que a lógica do seu CLP está correta — antes do deploy, não depois do incidente na madrugada.
Motor de verificação
ESBMC · Z3 / Bitwuzla
Origem
CETELI/UFAM · Manchester
Conformidade
NR-12
O problema
Quando a lógica falha, quem para é a máquina
A prensa, a esteira, o robô de solda — a célula inteira para. Não é uma tela travando: é produção parada, com o custo-hora correndo enquanto ninguém sabe exatamente onde está o erro.
A linha só volta quando alguém encontra o defeito no meio do turno, com o técnico lendo Ladder às três da manhã — incluindo falhas de concorrência que testes convencionais simplesmente não alcançam.
→ linha parada
→ técnico lendo o programa em produção
→ causa raiz ainda desconhecida
→ custo-hora acumulando
A solução
Verificação formal, não apenas mais testes
O ESBMC-PLC prova as propriedades da sua lógica Ladder com solvers SMT (Z3 e Bitwuzla) — encontrando a falha com a máquina ainda produzindo, antes do deploy chegar à planta.
O núcleo do verificador é aberto e auditável: você, ou um terceiro de sua confiança, reproduz a prova por conta própria. Os módulos premium — interface executiva e gerador de relatório NR-12 — são licenciados.
→ modelo formal da lógica Ladder
→ prova das propriedades críticas
→ falhas de concorrência incluídas
→ veredito antes do deploy
Como funciona
Do programa Ladder ao relatório de conformidade
Modelagem
Parametrização das regras de verificação em YAML, sem reescrever a lógica Ladder original do seu programa.
Verificação formal
O motor ESBMC executa a prova sobre o programa, incluindo condições de concorrência entre rungs.
Validação conjunta
Os engenheiros da sua fábrica e a nossa equipe confirmam juntos cada veredito, sobre a lógica da sua própria linha.
Relatório NR-12
Auditoria legível por técnicos, pronta para apoiar a conformidade da sua planta.
Para quem
Construído para quem sustenta a linha rodando
Multinacionais do PIM
Fábricas altamente automatizadas, dependentes de automação rígida por CLPs, nos setores eletroeletrônico e de duas rodas.
Integradores de sistemas
Engenharias que projetam e atualizam plantas no Distrito Industrial, e precisam garantir a lógica antes da entrega.
Gerências de operação e OT
Responsáveis pela continuidade operacional e pela integridade cibernética industrial da planta.
Base técnica
De onde vem o motor por trás da prova
CETELI / UFAM
Âncora local para infraestrutura de laboratório, ensaios de conformidade e rede regional no PIM.
University of Manchester
Cooperação científica internacional na evolução do núcleo algorítmico do solucionador ESBMC.
Núcleo aberto ESBMC
Motor premiado, com resolvedores SMT bit-vector integrados (Z3 e Bitwuzla), auditável por terceiros.
Suíte de benchmarks validada
Modelos industriais reais já testados, incluindo casos Controllino e MathWorks.
Contato
Converse com quem desenvolve o verificador
Sem camada intermediária. Conte um pouco sobre a sua planta e o número de máquinas envolvidas.