Abordagem de modelação de sistemas PLC (Parte 1)
3. Análise e aperfeiçoamento do modelo PLC
A secção anterior apresentou o sistema de modelação de PLC. De acordo com esta estratégia, podemos abstrair o sistema de PLC num modelo formal para verificação de modelos. Por conseguinte, a credibilidade deste modelo determinará diretamente os resultados da verificação do mesmo. Se o modelo não abranger completamente o sistema original (chamamos-lhe «menor do que o sistema original»), poderá fazer com que alguns erros não sejam detetados; se o sistema real cobrir completamente o modelo, mas este contiver muitos estados que o sistema original não possui (a que chamamos de «menor do que o sistema original»), o sistema original é extenso, o que pode introduzir alguns erros que não existem no sistema real. A isto chama-se um pseudo-erro. Assim, existem duas estratégias de modelação necessárias.
Em primeiro lugar, para detetar todos os erros no sistema, devemos construir um modelo suficientemente abrangente para cobrir todos os sistemas originais de estado; em segundo lugar, o modelo deve ser o mais fiel possível ao sistema real. Isto não só reduzirá o espaço de estados, como também melhorará a eficiência. Com base nos requisitos, iremos analisar o modelo de intervalos de tempo.
Proposição 1: Se o modelo de intervalos de tempo cumprir as propriedades, o modelo do sistema PLC real também as cumpre. A correção da Proposição 1 pode ser concluída a partir da relação entre os dois modelos. Isso significa que tudo o que irá acontecer ao modelo real está contido no modelo de intervalos de tempo; o modelo de intervalos de tempo é mais abrangente do que o modelo real. Se não for possível encontrar um contraexemplo utilizando o modelo de intervalo de tempo, é possível provar a correção do modelo real do PLC; por outro lado, se encontrarmos um contraexemplo, não é possível determinar se o sistema PLC real apresenta erros. Ou seja, o inverso da Proposição 1 é falso. É então necessária uma intervenção manual para analisar o contraexemplo e determinar se se trata de um erro espúrio.
A estratégia de modelação por intervalos de tempo permite obter um modelo resumido do PLC, e muitos estudos baseados no NuSMV também utilizam estratégias semelhantes ao modelo por intervalos de tempo para simular sistemas PLC. No entanto, o “modelo de intervalo de tempo” desvia-se significativamente do modelo real e necessita de ser aperfeiçoado. Este desvio deve-se ao facto de o “modelo de intervalo de tempo” não refletir as características de varredura de alta velocidade do PLC nem as características de varredura de baixa velocidade das entidades simultâneas. Ou seja, todas as alterações ambientais devem ser detetadas pelo PLC de alta velocidade, mas o modelo de intervalo de tempo ignora as características de alta velocidade do PLC, pelo que as alterações no ambiente externo podem não ser detetadas. Em resposta aos problemas acima referidos, tendo em conta as características físicas da varredura externa de alta velocidade e da simultaneidade de baixa velocidade, a estratégia de modelação por intervalo de tempo será melhorada através da adição de um mecanismo de espera de notificação. Com base no modelo de intervalo, cada entidade de estado simultâneo deve ser bloqueada e aguardar num determinado local após a conclusão da transferência. Só quando o controlador PLC tiver efetuado a leitura completa pelo menos uma vez é que o mecanismo de espera de notificação
A entidade concorrente elimina o bloco e continua a trabalhar. Em seguida, a transferência é concluída. O processo através do qual a entidade concorrente conclui a migração por meio do mecanismo de notificação em espera é ilustrado na Figura 2:
t0: A transmissão inicia, é interrompida e notifica o controlador PLC.
t1-tm: o PLC efetua uma leitura completa m vezes (m em
Pelo menos.
tm 1: A entidade concorrente recebe a notificação do PLC e a transferência é concluída.
Este mecanismo garante que cada alteração de estado de uma entidade simultânea possa ser detetada pelo controlador PLC pelo menos uma vez.
Proposta n.º 2
Após a adição do mecanismo de espera de notificações, o modelo passa a ser um subconjunto do modelo de intervalo de tempo. existe
Ao mesmo tempo, o modelo também pode incluir todas as situações do modelo real. Por outras palavras, se um modelo adicionar um mecanismo de espera de notificação que esteja em conformidade com os atributos, o modelo real do sistema PLC também estará em conformidade. A utilização da Proposição 1 para provar a Proposição 2 é semelhante. Através da Proposição 2, podemos verificar que o modelo do mecanismo continua a apresentar boas propriedades após a adição da espera por notificação. Conforme mencionado anteriormente, os modelos abstratos de sistemas têm dois requisitos: em primeiro lugar, que o sistema real esteja completamente incluído e, em segundo lugar, que o modelo seja o mais próximo possível do sistema real. A primeira proposição visa provar que o modelo de intervalos de tempo inclui o sistema real. Desde que se utilizem ferramentas de verificação de modelos para provar que o modelo abstrato satisfaz determinadas propriedades, as propriedades reais do sistema também as satisfarão. No entanto, este modelo não é exatamente igual ao modelo real; deve ser muito maior do que o modelo real. Em comparação com os modelos de intervalo de tempo, este modelo reduz ainda mais a distância entre os sistemas reais, diminuindo significativamente a probabilidade de detetar erros espúrios.
Uma ferramenta de verificação de modelos apresentará um contraexemplo que viole a propriedade do sistema; é fácil determinar manualmente se um contraexemplo num sistema real é verdadeiro ou não. Se o erro no sistema original existir realmente, então encontramos um contraexemplo. Caso contrário, o erro deve-se ao facto de o modelo abstrato ser mais abrangente do que o sistema real, tratando-se de um erro espúrio. Portanto, embora este modelo de intervalo de tempo não seja completamente equivalente ao sistema original, através deste modelo podemos avaliar se um sistema satisfaz uma determinada propriedade e, caso contrário, podemos encontrar um contraexemplo específico (são ainda necessárias mais verificações para determinar se se trata de um erro espúrio). O modelo não é equivalente ao sistema original principalmente porque existem muitos fatores difíceis de modelar no sistema real, alguns dos quais podem conduzir a erros. Se todos os fatores fossem modelados, isso resultaria na construção de um modelo gigantesco que não poderia ser verificado ou que simplesmente não poderia ser implementado. O modelo de intervalo de tempo abstrai fatores-chave do sistema real e modela-os, reduzindo significativamente o espaço de estados e a complexidade temporal. Ao mesmo tempo, através do mecanismo de espera de notificações, o modelo aproxima-se do sistema real, o que não só reduz a complexidade temporal, como também diminui os pseudoerros mencionados anteriormente.
A verificação NuSMV é implementada no modelo estabelecido acima. Formulámos uma série de regras de conversão para transpor o modelo acima 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 é semelhante à linguagem C, sendo ambas semanticamente semelhantes. Por isso, limitamo-nos a apresentar alguns exemplos para ilustrar os conceitos básicos da tradução. Para consultar informações detalhadas sobre a linguagem PROMELA, visite www.spinroot.com. Apresentaremos 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. Atribuímos o valor à porta de saída através da lógica.
Conta todas as portas de entrada. Esta é a tradução.
Método de rede PLC.
Verificação de modelos de PLC (Parte 3)
