El documento describe una metodología para validar la precisión de la implementación en tiempo de ejecución de un sistema de control. El tiempo de ejecución toma la forma de una máquina virtual que ejecuta código portátil conforme a las normas IEC 61131-3. Se ha diseñado un modelo formal, que comprende ecuaciones de semántica denotacional, para especificar la decodificación de instrucciones de máquina y operaciones, incluidas funciones aritméticas en varios tipos de datos, matrices y llamadas a subprogramas. El modelo también abarca mecanismos de manejo de excepciones para errores en tiempo de ejecución, como la división por cero y el acceso a índices de matriz inválidos. Este modelo denotacional se traduce a forma ejecutable utilizando el lenguaje funcional F. La verificación implica comparar la implementación real de la máquina virtual con este modelo ejecutable. Cualquier disparidad entre el modelo y la implementación indica desviaciones de la especificación. Implementado dentro del entorno de ingeniería CPDev, este enfoque garantiza una ejecución de programa de control consistente y predecible en diferentes plataformas objetivo.