Una contribución a las técnicas avanzadas de verificación de procesos de negocio y sistemas software abiertos

Abstract

La búsqueda de notaciones y lenguales para la descripción de Procesos de Negocio (Business Processes, BP) ha sido uno de los objetivos del Modelado de Procesos de Negocio (Business Process Modelling, BPM) en los últimos tiempos. Como resultado de este esfuerzo, la Notación para el Modelado de Procesos de Negocio (Business Process Modelling Notation, BPMN) ha surgido como una notación gráfica estandarizada ampliamente aceptada para la documentación de BP. Sin embargo, por la heterogeneidad de sus construcciones y por la falta de una definición precisa de la notación, la especificación, el modelado y la verificación formal de BP se ve obstaculizado. En esta tesis doctoral, como parte de los trabajos relacionados con las Herramientas Metodológicas para la Verificación de Sistemas Abiertos y Procesos de Negocio, se presenta una propuesta para la especificación, el modelado y la verificación composicional de requisitos no funcionales y restricciones temporales de modelos de BP realizados con BPMN. Para la especificación y el modelado se define una semántica formal de los elementos notacionales de tiempo de BPMN, bajo el dominio semántico del cálculo de proceso basado en CSP, Communicating Sequential Processes + Time (CSP+T). Para la verificación formal de los modelos de BP se utiliza el Enfoque Formal de Verificación Composicional (EFVC), una propuesta que se hace en el ámbito de la Ingeniería de Software (IS) para la verificación composicional de Sistemas con Criticidad en Seguridad (Safety-Critical Systems, SCS), que integra la verificación composicional con la técnica de verificación automática Model Ckecking (MC). Como resultado, se ha obtenido una herramienta metodológica que incorpora avances de la IS al ámbito del BPM para el análisis formal de modelos de BP. Además, se presenta el diseño general del conjunto de herramientas de software que permiten automatizar el EFVC y se describe la implementación de la herramienta BTransformer, la cual soporta la transformación de modelos BPMN a términos de proceso CSP+T. Adicionalmente, se discute la aplicación de los aportes de la presente tesis doctoral a dos casos de interés empresarial e industrial. Uno, relacionado con un BP considerado crítico para la estrategia de Gestión de las Relaciones con el Cliente (Customer Relationship Management, CRM). El otro, corresponde al sistema que implementa el proceso crítico del protocolo de comunicación que constituye el corazón de una red de comunicación de teléfonos móviles. La aplicación del EFVC nos ha permitido corroborar que éste puede ser utilizado para verificar tanto el comportamiento de BP con criticidad, como los componentes que conforman el software que implementa BP complejos y con criticidad, conformando así una contribución dentro del área de las Técnicas Avanzadas de Verificación de BP y Sistemas Software Abiertos.