Verificación automática de procesos de negocio con un enfoque composicional.

• Luis Mendoza Morales Universidad Simón Bolívar-Venezuela
• Manuel Capel Tuñón Universidad de Granada-España
• María Pérez Universidad Simón Bolívar-Venezuela

Palabras clave: procesos de negocio, modelo de tareas, verificación automática, verificación composicional, especificación formal

Resumen

En la actualidad, los Procesos de Negocio (PN) complejos son implementados por Sistemas de Información Empresariales (SIE). Sin embargo, el desarrollo de los SIE se ve dificultado sino se garantiza la confiabilidad del Modelo de Tareas (MT) de los PN. Este artículo describe el Enfoque Formal de Verificación Composicional (EFVC); una infraestructura para la especificación formal y verificación de PN, soportado por técnicas de Verificación Automática (VA). Basado en una propuesta de semántica formal temporal para la Business Process Model and Notation (BPMN) que permite obtener el MT de un proceso de negocio, el EFVC soporta la verificación del comportamiento del MT a partir de la verificación individual de sus participantes. La interpretación de los elementos notacionales de BPMN en el lenguaje formal Communicating Sequential Processes + Time (CSP+T) nos permite incorporar herramientas de VA ampliamente utilizadas para verificar el comportamiento de un MT. Se presenta un ejemplo de aplicación real en el área del Manejo de las Relaciones con el Cliente (conocido como CRM) para demostrar el uso práctico de EFVC.