MÉTODO PARA TRADUÇÃO AUTOMÁTICA DE LÓGICA LADDER PARA UM VERIFICADOR DE MODELO COM BASE EM SMT EM UMA REDE

IPC Classification

Priority claims

Abstract

MÉTODO PARA TRADUÇÃO AUTOMÁTICA DE LÓGICA LADDER PARA UM VERIFICADOR DE MODELO COM BASE EM SMT EM UMA REDE. A presente invenção refere-se a um método para tradução automática de lógica ladder para um verificador de modelo com base em SMT em uma rede compreendendo definir (10) a topologia da rede como uma topologia de rede enriquecida com base em pacotes trocados na rede, extrair (20) um programa a partir dos pacotes relativos a um PLC na rede e identificar entradas, saídas, variáveis e um diagrama ladder do PLC, traduzir (30) as entradas, saídas, variáveis e diagrama ladder em um modelo formal predefinido, em que o modelo formal predefinido é um verificador de modelo com base em SMT tipo circuito, e em que a tradução (30) compreende traduzir o conjunto de tipos de dados do programa de acordo com um conjunto de modelos predefinido de tipos de dados do verificador de modelo com base em SMT tipo circuito, traduzir as entradas do PLC como entradas de modelo do verificador de modelo com base em SMT tipo circuito do mesmo tipo, traduzir as saídas do PLC como travas de saída de modelo do verificador de modelo com base em SMT tipo circuito do mesmo tipo, traduzir as variáveis do PLC como travas de variável de modelo do verificador de modelo com base em SMT tipo circuito do mesmo tipo, traduzir comparadores e operadores aritméticos do diagrama ladder em uma pluralidade de funções de modelo predefinidas do verificador de modelo com base em SMT tipo circuito, traduzir contatos e bobinas do diagrama ladder de acordo com procedimentos recursivos de modelo predefinidos relacionados ao conjunto de modelos predefinidos de tipos de dados, as entradas de modelo, as travas de saída de modelo, as travas de variável de modelo e a pluralidade de funções de modelo predefinidas, em que os contatos são chaves que podem bloquear ou permitir o fluxo da corrente em uma conexão e cada um dos contatos é controlado por uma entrada ou variável booleana, e em que as bobinas atribuídas a variáveis booleanas.