Enfoque Formal de Verificación y Autómatas Temporizados Aplicados a Procesos Industriales

Resumen

Una de las metas de la Ingeniería de Software y del Modelado de Procesos de Negocio es lograr que los diseñadores de negocios y los desarrolladores de sistemas construyan aplicaciones de software confiables, principalmente para aquellos Procesos Industriales Críticos (PIC); es decir, aquellos procesos que impactan directamente la misión de una industria. El uso de Métodos Formales, tales como la técnica de Verificación Automática y la teoría de Autómatas Temporizados (AT), ha demostrado que propicia la confiabilidad y la seguridad de PIC al aumentar su comprensión, revelando inconsistencias, ambigüedades e incompletitudes, que de otra manera pasan desapercibidas. Este trabajo presenta la integración de un Enfoque Formal de Verificación (EFV) con la teoría de AT para la especificación y la verificación automática del Modelo de Tareas (MT) asociado a un PIC (MTPI). Además, se introducen un conjunto de directrices para transformar modelos de PIC en AT. El resultado del uso del EFV con la verificación automática y los AT es una infraestructura metodológica que garantiza la exactitud del MTPI con respecto a la especificación de las propiedades iniciales derivadas de las buenas prácticas o reglas de negocio de una industria. Con el fin de mostrar la viabilidad de la propuesta, se discute el caso Celda de Producción, un típico ejemplo para evaluar metodologías para el diseño de sistemas industriales, el cual ilustra cómo integrar la verificación automática en las etapas tempranas del diseño de PIC.