4. Verificação do modelo de PLC
O PLC é amplamente utilizado em muitas aplicações e tem muitos dispositivos; é uma grande área de investigação. Qualquer trabalho de PLC envolve diferentes equipamentos e pessoas, pelo que o sistema PLC é concorrente.
Se houver alguns erros no sistema PLC que são difíceis de encontrar, eles são principalmente devido a erros de design lógico, mas não erros de cálculo, por isso nos concentramos no processo de lógica do programa de deteção PLC, e esta lógica pode completamente
Descrição da lógica de bits. Por conseguinte, para simplificar o modelo do programa PLC e concentrarmo-nos na verificação do modelo, efectuamos as seguintes configurações:
O PLC é um programa de controlo lógico e todas as variáveis de controlo têm apenas dois estados: 0 e 1;
Os programas PLC são executados num ambiente concorrente. Neste caso, é mais provável que a programação do PLC tenha alguns erros que não são fáceis de encontrar. Tendo em conta as caraterísticas acima referidas, utilizamos a ferramenta de verificação de modelos SPIN (o nosso PLC-Checker também implementa o NuSMV no modelo estabelecido acima) para inspeção. Formulámos uma série de regras de conversão para construir o modelo acima na linguagem de entrada do SPIN, o Promela. Os atributos do sistema também precisam de ser traduzidos para Promela. O SPIN junta-os e depois efectua a deteção. A linguagem PROMELA é uma linguagem do tipo C e são semanticamente semelhantes, pelo que vamos apenas dar alguns exemplos
Mostra conceitos básicos de tradução. Para ver informações detalhadas sobre a linguagem PROMELA, visite www.spin root.com. Vamos apresentar as três partes do ficheiro PRO MELA como entrada para o SPIN.
1) Código do controlador PLC
Um controlador PLC é composto por várias redes.
O código para o controlador PLC também é gerado a partir da rede. É claro que, antes de fazer isso, é preciso declarar as variáveis necessárias. Cada rede tem suas portas de entrada e saída, e cada porta pode ser representada por uma expressão booleana.
Contar todas as portas de entrada. Esta é a tradução
Método de rede PLC.
Eis um exemplo de conversão de uma rede SR:
if ::Exp(R) == 1 -> Q = 0; ::else -> if ::Exp(S) == 1 -> Q = 1; ::else -> skip; fi; fi; /* Exp(S) é a expressão booleana da porta S Exp(R) é a expressão booleana da porta R Q é a porta de saída */
2) Código das entidades concorrentes
Acreditamos que cada entidade concorrente é um processo único, independentemente do comportamento humano ou do equipamento. Estes processos partilham variáveis com o processo do controlador PLC. Isso deve ser feito para garantir a simultaneidade do sistema. Na segunda parte deste artigo, discutimos que todas as entidades concorrentes são modeladas como autómatos. Este autómato significa passar de um estado para outro. Usamos portas I para formar o estado da entidade. Utilizamos instruções goto como saltos (tal como na linguagem assembly). Um exemplo simples é o seguinte:
atómico { if :: Q1 -> {IB, vai para o estadoB} :: Q2 -> {IC, ir para o EstadoC} fi;} /* EstadoA é a etiqueta do Estado A Q1, Q2 é a condição de transferência IB é definir o valor do estado para o valor do estado B goto EstadoB significa saltar para o estadoB */
3) Código do imóvel
As propriedades são regras que o sistema PLC deve cumprir. Utilizamos a fórmula LTL (Linear Time Logic) como formato de entrada. Devemos escrever a propriedade oposta devido ao mecanismo do SPIN. O SPIN vai descobrir que a nossa propriedade de caso acontece, o que deve ser um contra-exemplo. Não podemos escrever a fórmula LTL diretamente, mas sim utilizar a macro ing. Primeiro devemos definir todas as proposições em macros em LTL (como #define p i5 == 0), depois usamos as proposições definidas para formar fórmulas LTL. O Spin pode converter automaticamente as fórmulas LTL em códigos PRO MELA utilizando o comando "SPIN-f" (ver mais pormenores no manual SPIN).
4) Mecanismo de espera de notificação
Na discussão sobre a modelação, recomendamos que não se adicione um mecanismo de tempo de espera. Este mecanismo também tem de ser refletido no código. A implementação específica é assinar uma variável bit de cada processo não-PLC (exceto todos os controladores PLC do processo) como um sinal. Quando o autómato transita para uma etiqueta de estado, a variável de sinal é colocada a 0, e a próxima atribuição requer que esta variável seja 1 para continuar. Este processo continua devido às caraterísticas da sintaxe do PROMELA. Não existe tal restrição no processo PLC. Em vez disso, o processo PLC pode definir estas variáveis para 1, assegurando assim que cada passo deve ser completado através de pelo menos um scan PLC. A isto chama-se um mecanismo de espera de notificação.
Seguindo os quatro passos acima, obtemos um ficheiro de entrada SPIN completo para o nosso sistema. Podemos então utilizar o SPIN para verificar o modelo. Para um verificador passo a passo do modelo SPIN, consulte o manual SPIN (visite www.spin root.com). O SPIN dá-nos o resultado se for encontrado um contra-exemplo. Podemos usar a teoria para analisar o ficheiro de rastreio dado pelo spin mencionado acima. Utilizando este mecanismo de deteção, desenvolvemos uma ferramenta de verificação de modelos PLC-checker. Esta ferramenta ajuda a construir modelos visuais e a efetuar inspecções, e pode fornecer uma análise simples dos resultados. Naturalmente, o contra-exemplo que encontra deve ser verificado manualmente para determinar se é um verdadeiro contra-exemplo. No entanto, com a ajuda de ficheiros de rastreio, esta não é uma tarefa muito difícil. Também utilizámos com sucesso alguns verificadores PLC (apresentados na secção seguinte). No exemplo clássico do livro de texto, foi encontrado um contra-exemplo. Embora a probabilidade de contra-exemplos seja muito baixa, eles ocorrem e podem ter consequências graves. Esta ferramenta também prova a correção e a validade da teoria deste artigo.
5. Executar o PLC-Checker
Vamos demonstrar a eficácia do verificador PLC na verificação do modelo de canal de duas portas da seguinte forma. Duas portas de passagem são utilizadas para isolar a sala do mundo exterior.
Ao introduzir o diagrama ladder e as entidades concorrentes na ferramenta, que é a definição das propriedades, efectuamos uma verificação. A Figura 3 mostra os resultados. Como podemos ver, existe um erro no resultado. Este facto é comprovado pela verificação das pistas como sendo um verdadeiro contra-exemplo ao arquivamento manual. Ou seja, o nosso mecanismo é eficaz na verificação de tais programas PLC.
6. Em conclusão
Neste artigo, estudamos a teoria de modelação e verificação de PLC utilizando métodos formais. Os requisitos analisam as caraterísticas da modelação de PLC e estabelecem um modelo de entidade concorrente através da estratégia de intervalo de tempo. Em seguida, provamos que o modelo de intervalo de tempo é um superconjunto de sistemas PLC e reduzimos o modelo adicionando um mecanismo de espera sem tempo. Também garante que todas as alterações ao sistema podem ser analisadas pelo controlador do PLC. Descobrimos que podemos encontrar erros num sistema examinando os seus contra-exemplos. Finalmente, é apresentada a utilização do SPIN para verificar o modelo. Há também uma introdução correspondente à ferramenta de verificação do modelo PLC-Checker. Nesta fase, o mecanismo é ainda muito imperfeito, tal como o seu processamento como temporizador. Mas tem grandes e únicas vantagens para resolver problemas de exploração de estados. Estamos ainda a explorar ativamente estas questões.