Abordagem de modelação de sistemas PLC (Parte 1)
Análise e Melhoria de Modelos PLC (Parte 2)
4. Verificação do modelo do PLC
O PLC é amplamente utilizado em muitas aplicações e conta com diversos dispositivos; trata-se de uma vasta área de investigação. Qualquer trabalho com PLC envolve diferentes equipamentos e pessoas, pelo que o sistema PLC é concorrente. Ao mesmo tempo, se existirem alguns erros num sistema PLC, é difícil identificá-los, principalmente devido a erros de conceção lógica, e não a erros de cálculo. Por conseguinte, centramo-nos no processo lógico do programa de deteção do PLC, e esta lógica pode ser totalmente descrita através da lógica de bits. Assim, para simplificar o modelo do programa do PLC e centrar-nos na verificação do modelo, nós
Defina as seguintes opçõ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 de PLC são executados num ambiente simultâneo. Neste caso, é mais provável que a programação do PLC contenha alguns erros que não são fáceis de detetar.
Tendo em conta as características acima referidas, utilizamos a ferramenta de verificação de modelos SPIN (a nossa ferramenta PLC-Checker também implementa o NuSMV) para efetuar a verificação. Formulámos uma série de regras de conversão para transpor o modelo acima referido para a linguagem de entrada do SPIN, a Promela. Os atributos do sistema também têm de ser traduzidos para Promela. O SPIN reúne-os e, em seguida, realiza a deteção.
A linguagem PROMELA é uma linguagem semelhante à C, sendo ambas semanticamente semelhantes. Por isso, apresentamos apenas alguns exemplos para ilustrar os conceitos básicos de tradução. Para consultar informações detalhadas sobre a linguagem PROMELA, visite www.spinroot.com. Iremos apresentar as três partes do ficheiro PROMELA 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 o fazer, deve declarar as variáveis de que necessita. Cada rede tem as suas portas de entrada e saída, e cada porta pode ser representada por uma expressão booleana. Calculamos todas as portas de entrada atribuindo logicamente os valores das portas de saída. É assim que se traduz uma rede de PLC.
Eis um exemplo de conversão de uma rede SR:
se
::Exp(R) == 1 -> Q = 0;
::Outros->
if::Exp(S) == 1 -> Q = 1;
::else -> ignorar; faisão;
Fei;
/* Exp(S) é a expressão booleana da porta S
Exp(R) é uma expressão booleana para a 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:
Estado A:
atom{
se
:: Q1 -> {IB, saltar para o Estado B}
:: Q2 -> {IC, saltar para StateC}
Filipinas;}
/* StateA é a designação do estado A
Q1 e Q2 são condições de transferência
O IB deve definir o valor do estado para o valor do estado B
goto StateB significa saltar para o estado B */
3) O código de propriedade é uma regra que o sistema PLC deve cumprir. Utilizamos uma fórmula LTL (Lógica Temporal Linear) como formato de entrada. Devemos escrever a propriedade oposta devido ao mecanismo do SPIN. O SPIN irá concluir que a nossa propriedade de caso se verifica; isso deve constituir um contraexemplo. Não podemos escrever a fórmula LTL diretamente, mas devemos utilizar a macro «ing». Em primeiro lugar, devemos definir todas as proposições.
Numa macro em LTL (como, por exemplo, #define p i5 == 0), utilizamos a proposição definida para formar a fórmula LTL. O Spin pode converter automaticamente fórmulas LTL em códigos PRO MELA utilizando o comando “SPIN-f” (consulte mais detalhes no manual do SPIN).
4) Mecanismo de espera de notificação
Na discussão sobre a modelação, recomendamos que não se adicione um mecanismo de espera. Este mecanismo também tem de ser refletido no código. A implementação específica consiste em assinar uma variável de bits de cada processo não-PLC (exceto todos os controladores PLC de processo) como um sinal. Quando o autómato transita para um rótulo de estado, a variável de sinal é definida como 0, e a atribuição seguinte requer que esta variável seja 1 para continuar. Este processo prossegue devido às caracterí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 como 1, garantindo assim que cada passo deve ser concluído ao longo de, pelo menos, uma varredura do PLC. Isto denomina-se mecanismo de espera por notificação. Seguindo os quatro passos acima, obtemos um ficheiro de entrada SPIN completo para o nosso sistema. Depois, podemos utilizar o SPIN.
Verifique o modelo. Para um guia passo a passo sobre o modelo SPIN, consulte o manual do SPIN (visite www.spinroot.com). O SPIN indicará se foi encontrado algum contraexemplo. Podemos utilizar a teoria para analisar o ficheiro de acompanhamento fornecido pelo SPIN, mencionado acima.
Utilizando este mecanismo de deteção, desenvolvemos uma ferramenta para verificação de modelos, o PLC-checker. Esta ferramenta facilita a criação de modelos visuais e a implementação de inspeções, além de permitir uma análise simples dos resultados. É claro que o contraexemplo que a ferramenta encontra deve ser verificado manualmente para determinar se se trata de um verdadeiro contraexemplo. No entanto, com a ajuda de ficheiros de registo, esta não é uma tarefa muito difícil. Também utilizámos com sucesso alguns verificadores de PLC (apresentados na secção seguinte). No exemplo clássico dos livros didáticos, foi encontrado um contraexemplo. Embora a probabilidade de contraexemplos seja muito baixa, estes ocorrem e podem ter consequências graves. Esta ferramenta também comprova a correção e a validade da teoria apresentada neste artigo.
5. Executar o PLC-Checker
Iremos demonstrar a eficácia do verificador PLC na verificação do modelo de canal de duas portas da seguinte forma. É utilizada uma passagem com duas portas para isolar a sala do mundo exterior. Ao introduzir o diagrama de escada e as entidades simultâneas na ferramenta, o que constitui a definição das propriedades, procedemos à verificação. A Figura 3 mostra os resultados. Como se pode ver, existe um erro no resultado. Isto é comprovado pela verificação das pistas, que constituem um contraexemplo real à verificação manual. Ou seja, o nosso mecanismo é eficaz na verificação destes programas PLC.
6. Em conclusão
Neste artigo, estudamos a teoria da modelação e verificação de PLC utilizando métodos formais. A análise de requisitos examina as características da modelação de PLC e estabelece um modelo de entidade concorrente através de uma estratégia de intervalos de tempo. Em seguida, demonstramos que o modelo de intervalos de tempo é um superconjunto dos sistemas PLC e reduzimos o modelo através da adição de um mecanismo de espera sem restrições temporais. Isto também garante que todas as alterações no sistema possam ser detetadas pelo controlador PLC. Descobrimos que é possível identificar erros num sistema através da análise dos seus contraexemplos. Por fim, é apresentada a utilização do SPIN para verificar o modelo. É também fornecida uma introdução correspondente à ferramenta de verificação de modelos PLC-Checker. Nesta fase, o mecanismo ainda apresenta muitas imperfeições, tais como o tratamento dos temporizadores. No entanto, possui vantagens significativas e únicas para resolver problemas de exploração de estados. Continuamos a explorar ativamente estas questões.
