3) Entidades comportamentais humanas
Definição 2.2. A entidade de comportamento humano é uma tupla Env=
As entidades comportamentais humanas são semelhantes às entidades de hardware;
Têm a mesma definição de estado. É difícil simular o comportamento humano, especialmente quando a conceção de um autómato envolve um certo número de indivíduos. Em resposta a estas dificuldades, a modelação do comportamento humano deve adotar um processo iterativo: em primeiro lugar, constrói-se um modelo comportamental simples utilizando a validação do modelo; em seguida, se não for encontrado um contra-exemplo, constrói-se e verifica-se um modelo mais complexo até se encontrar um contra-exemplo ou mais difícil de encontrar. Complexo; finalmente, se nenhum contra-exemplo significativo for encontrado antes, é gerado um modelo de comportamento humano completamente aleatório (ou seja: o comportamento humano é um grafo completo e todas as transferências são verdadeiras) para verificação. No entanto, a verificação de um comportamento completamente aleatório conduzirá a um aumento acentuado do espaço de estados, pelo que a escolha de um modelo de comportamento humano adequado é um ponto difícil na modelação. Se a entrada humana for relativamente simples, podemos utilizar a modelação do comportamento completamente aleatório, caso contrário, é necessário considerar seriamente a construção de um modelo razoável do comportamento humano.
Modelamos o comportamento do ambiente do PLC e das pessoas, e depois modelamos o controlador do PLC. O controlador PLC estará num ciclo quando estiver a rodar.
O PLC lê todas as entradas da porta I.
O PLC calcula todas as unidades lógicas.
PLC define todos os portos Q.
A unidade básica no processo PLC é chamada de rede. Todas as redes serão executadas por ordem numerada para configuração em tempo de projeto.
A rede de operações lógicas básicas do controlador PLC inclui: Flip-flop S, flip-flop R, flip-flop SR, flip-flop EQ, flip-flop RS, detetor de borda ascendente POS, detetor de borda descendente NEG, etc. Para modelar a rede de operações lógicas básicas, adoptamos uma estratégia de mapeamento direto, ou seja, o modelo do controlador do comportamento da rede PLC é completamente equivalente ao comportamento lógico da rede. Os flip-flops R, SR, EQ e RS podem ser diretamente mapeados para o seu comportamento através de expressões booleanas.
3. Análise e melhoria do modelo PLC
A secção anterior introduziu o sistema de modelização do PLC. De acordo com esta estratégia, podemos abstrair o sistema PLC num modelo formal para a verificação do modelo. Por conseguinte, a credibilidade deste modelo determinará diretamente os resultados da verificação do modelo. Se o modelo não cobrir completamente o sistema original (chamamos-lhe mais pequeno do que o sistema original), pode fazer com que alguns erros não sejam detectados; se o sistema real puder cobrir completamente o modelo, mas contiver muitos estados que o sistema original não tem (chamamos-lhe mais pequeno do que o sistema original), o sistema original é grande), 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 encontrar todos os erros no sistema, devemos construir um modelo suficientemente grande para cobrir todos os sistemas originais de estado; em segundo lugar, o modelo deve estar o mais próximo possível do sistema real. Isto não só reduzirá o espaço de estados, como também melhorará a eficiência. Com base nestes requisitos, vamos analisar o modelo de intervalo de tempo. Proposição 1 Se o modelo de intervalo de tempo estiver em conformidade com as propriedades, o modelo do sistema PLC real também está em conformidade. A correção da proposição 1 pode ser concluída a partir da relação entre os dois modelos. Isto significa que tudo o que acontecerá ao modelo real está contido no modelo de intervalo de tempo, o modelo de intervalo de tempo é maior do que o modelo real. Se não conseguirmos encontrar um contra-exemplo utilizando o modelo de intervalo de tempo, podemos provar a correção do modelo real de PLC; por outro lado, se encontrarmos um contra-exemplo, não podemos determinar se o sistema real de PLC tem erros. Ou seja, o inverso da proposição 1 é falso. É então necessária uma intervenção manual para analisar o contra-exemplo e determinar se se trata de um erro espúrio. A estratégia de modelação por intervalos de tempo pode 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 modelar sistemas PLC. No entanto, o “modelo de intervalo de tempo” desvia-se muito do modelo real e precisa de ser melhorado. Este desvio é o seguinte: o “modelo de intervalo de tempo” não reflecte as caraterísticas de digitalização a alta velocidade do PLC e as caraterísticas de digitalização a baixa velocidade das entidades concorrentes, ou seja, todas as alterações do ambiente devem ser digitalizadas
O PLC de alta velocidade, mas o modelo de intervalo de tempo ignora as caraterísticas de alta velocidade do PLC, pelo que as alterações no ambiente externo podem não ser analisadas.
As propriedades físicas e as estratégias de modelação de intervalos de tempo serão melhoradas através da adição de um mecanismo de espera de notificação. Com base no modelo de intervalo, cada entidade de estado concorrente deve ser bloqueada e aguardar algures após a conclusão da transferência. Só quando o controlador PLC tiver efectuado uma varredura completa pelo menos uma vez, o mecanismo de notificação em espera enviará uma mensagem à entidade concorrente para remover o bloqueio e continuar a trabalhar. A transferência é então concluída. O processo de migração de entidades concorrentes através do mecanismo de espera sem tempo é mostrado na Figura 2:
Este mecanismo garante que o controlador do autómato analisa cada mudança de estado das entidades concorrentes pelo menos uma vez. Proposição 2 Após a adição do mecanismo de notificação em espera, o modelo torna-se um subconjunto do modelo de intervalos de tempo. 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 notificação em espera que esteja em conformidade com os atributos, o modelo real do sistema PLC também está em conformidade.
A utilização da Proposição 1 para provar a Proposição 2 é semelhante. Através da Proposição 2, podemos ver que o modelo do mecanismo continua a ter boas propriedades após a adição da notificação em espera. Como mencionado anteriormente, os modelos abstractos de sistemas têm dois requisitos: primeiro, que o sistema real seja completamente incluído e, segundo, que o modelo seja o mais próximo possível do sistema real. A primeira proposição é provar que o modelo de intervalo 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, então as propriedades reais do sistema também as satisfarão. Mas 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 intervalos de tempo, este modelo reduz ainda mais a distância entre os sistemas reais, reduzindo consideravelmente a possibilidade de detetar erros espúrios. Uma ferramenta de verificação de modelos dará um contra-exemplo que viola a propriedade do sistema; é fácil determinar manualmente se um contra-exemplo num sistema real é verdadeiro ou não. Se o erro no sistema original existir de facto, então encontramos um contra-exemplo. Caso contrário, o erro deve-se ao facto de o modelo abstrato ser maior do que o sistema real, o que constitui um erro espúrio. Por conseguinte, 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, em caso afirmativo, podemos encontrar um contra-exemplo específico (são ainda necessárias mais verificações para determinar se se trata de um pseudo-erro). O modelo não é equivalente ao sistema original, principalmente porque há muitos factores que são difíceis de modelar no sistema real, alguns dos quais podem conduzir a erros. Se todos os factores fossem modelados, isso levaria à construção de um modelo enorme que é impossível de verificar, ou simplesmente impossível de implementar. O modelo de intervalos de tempo abstrai os factores-chave do sistema real e modela-os, reduzindo consideravelmente o espaço de estados e a complexidade temporal.
Ao mesmo tempo, através do mecanismo de espera de notificação,
O modelo torna-se mais próximo do sistema real, o que não só reduz a complexidade temporal, como também reduz os pseudo-erros mencionados anteriormente.