Expressing Temporized Properties in Ladder Diagrams

Abstract

Esse trabalho foi realizado dentro do grupo Vertics do LAAS-CNRS, Laboratório de Análise e Arquiteturas de Sistemas, localizado em Toulouse (França). Vertics possui um foco no estudo de métodos formais, em particular model checking, com o objetivo de desenvolver técnicas e ferramentas para aumentar a expressividade e escalabilidade destas. Model checking é uma poderosa ferramenta para tratar de sistemas discretos, capaz de expressar propriedades complexas além de manter a problemática resultante da explosão combinatória de estados sob controle. Nessa monografia, eu procuro expandir uma ferramenta de formalização de diagramas Ladders, uma linguagem de programação para PLCs, Programadores Lógicos controláveis, amplamente usados em vários setores industrias. A ferramenta, inicialmente concebida no trabalho [1] de Ana Maria Carpes, foi pensada como uma forma de ajudar técnicos e engenheiros treinados em Ladder, mas com pouco, ou nenhum, conhecimento em métodos formais. O objetivo dessa ferramenta é fornecer a estes um método para automatizar a verificação de diagramas Ladder e aumentar a confiabilidade em seus sistemas, em comparação ao simples uso de caso de testes e simulações. Durante o meu estágio, eu racionalizei a cadeia de ferramentas de verificação Ladder e reimplementei partes da ferramenta. Em particular, eu reimplementei a parte da cadeia de ferramenta responsável por importar diagramas Ladder criados no formato TC6, um formato open-source usado pelo programa PLCOpen editor. PLCOpen foi desenvolvido pela organização Beremiz como plataforma de desenvolvimento unificada para programs de PLC. O resultado de meu trabalho é uma ferramenta mais fácil de usar e mais integrada. Deveras, eu tornei acessível diferentes transformações em uma única ferramenta que é mais fácil de instalar e de manter. A ferramenta, que realiza 3 passos de transformação, tem como linguagem alvo Fiacre. Fiacre, uma linguagem formal criada especialmente para servir de fase intermediaria para definição de modelos formalizados, permite descrever comportamentos sequenciais e paralelos, através de processos e componentes. Em sequência, eu motivo não só a necessidade de aplicar verificação formal para sistemas, mas como ferramenta para verificar a solidez da ferramenta de verificação em si. Por exemplo, eu uso a noção de observadores para verificar a implementação de timers, um Bloco Complexo usado para implementar timeouts. Observadores nada mais são que componentes formais que analisam um modelo, sem que modifiquem a execução deste. O observador descrito nesse trabalho me permitiu descobrir um bug antes não detectado no comportamento temporal do modelo formal gerado para o bloco TON (Timer ON). Outra contribuição que faço é um método para definir propriedades de programas Ladders baseado em Matrizes Causa e Efeito (C&E Matrix), uma notação usada na industria para especificar diagramas Ladder. Ao final, eu explico algumas limitações da ferramenta e dos frameworks usados, já que o modelo de desenvolvimento, MDE (Model Driven Environment), apesar de facilitar o desenvolvimento de cada passo da transformação isoladamente, não fornece muito suporte quando as diversas partes são conectadas, levando a algumas questões a serem respondidas para desenvolvimento futuro. Indico também uma deficiência do ferramental de verificação formal de diagramas Ladder: falta uma ferramenta para traduzir os rastros de erros gerados, que não estão em um formato amigável para um usuário com pouco treino em ferramentas formais. Proponho então uma ferramenta de pós processamento do rastro de erros. Eu concluo que a ampliação de especificações básicas que um programa Ladder, através de observadores, são não somente uma maneira de garantir a validade da ferramenta, mas um caminho para desenvolver uma linguagem de alto nível para a definição de especificações formais de programas Ladder.

This work was performed within the VERTICS group, at LAAS-CNRS. This research group is actively seeking improvements to current tooling in formal methods, in particular based on model checking. My objective during this internship was to expand a tool for the formal verification of Ladder Diagrams. This tool, originally created by Ana Maria Carpes [1], was developed with the intent to help technicians and engineers that are trained on Ladder programming but that have no, or limited knowledge, of formal methods. The goal is to provide them with a way to automatize the validation of Ladder diagrams and to increase the trust on their system compared to the simple use of test cases and simulations. During my internship, I have streamlined the Ladder verification tool-chain and reimplemented parts of the tool. In particular, I have reimplemented the part of the tool-chain responsible for importing Ladder diagrams created using the TC6 exchange format. The end result is a tool that is easier to use and that is better integrated. Indeed, I have made accessible different transformations inside a single tool that is easy to install and to maintain. Another contribution of my work is a method for defining formal properties of Ladder programs based on Cause and Effect Matrices (C&E Matrix), a notation used in the industry for expressing the specification of Ladder diagrams. In this report, I motivate the need to apply formal verification to systems but also as a tool to check the soundness of the verification tool itself. For instance, I use the notion of observers to check the implementation of timers, a complex block in Ladder diagrams that can be used to model timeouts. With this work, I was able to uncover an undetected bug on the temporal behaviour of the formal models generated with our tools.