Los flujos de trabajo coordinan una serie de tareas computacionales para crear una lógica de flujo de trabajo sofisticada. Asegurar la corrección de una especificación de flujo de trabajo es esencial para automatizar procesos empresariales. Los errores en la especificación deben ser identificados y resueltos lo antes posible, durante la fase de diseño. En este artículo, proponemos un enfoque de verificación para especificaciones de flujo de trabajo utilizando técnicas de verificación de modelos. Introducimos un método para verificar las propiedades de corrección de los procesos de flujo de trabajo utilizando nuestro verificador de modelos de Lógica Temporal Alternante (ATL) embebido en la base de datos. Primero, la especificación del flujo de trabajo se traduce en una estructura de juego concurrente (CGS). A continuación, la propiedad deseada se expresa como una fórmula ATL. Finalmente, se ejecuta el verificador de modelos ATL para verificar si las propiedades de corrección se mantienen para el modelo. Para apoyar a los usuarios en la formalización de restricciones empresariales, la solución propuesta implementa un asistente basado en inteligencia artificial generativa. Los resultados experimentales muestran que el uso del método de inducción de cadena de pensamiento mejora significativamente el rendimiento del proceso de razonamiento al utilizar el modelo GPT-4o.