Verificación de programas escritos en PLC para entornos industriales

Abstract

[ES] En la primera parte del proyecto, abordamos la importancia de la verificación de programas desarrollados para dispositivos lógicos programables, también denominados PLC, que se han convertido en un elemento muy importante de la producción industrial y medios de transporte como, por ejemplo, el ferroviario. Para determinar mejoras en las soluciones actuales de verificación, realizamos un análisis de la tecnología disponible y entornos de programación de los dispositivos PLC. Dicho análisis servirá como base para realizar el estudio y puesta en práctica de una semántica formal ejecutable. Finalmente podremos ver el resultado de los programas PLC, siendo capaces de realizar su ejecución en el nuevo entorno y con el mínimo de modificaciones posibles respecto del programa original, y así poder comprobar la corrección en términos lógicos.

[EN] In the first part of the project, we address the importance of the verification of programs developed for programmable logic devices, also called PLCs, which are a very important element in industrial production and transport systems such as railways. To determine the improvements to existing verification solutions, we perform an analysis of the available technology and programming environments of PLC devices. This analysis will serve as the basis for the study and implementation of an executable formal semantics. Finally, we can see the result of the PLC programs, where we can carry out their execution in the new environment and with the minimum possible modifications with respect to the original program, and thus be able to verify the correctness in logical terms.