Las tecnologías de gestión de procesos de negocio supusieron,
en los años 90, una revolución en la forma de
coordinar las actividades internas de organizaciones,
principalmente de tamaño grande o mediano.
Posteriormente, a principios de esta década, el ámbito de utilización
de estas tecnologías comenzó su expansión a entornos B2B,
como un facilitador de las colaboraciones entre distintas organizaciones.
Ahora, están comenzando a ser aplicadas para
realizar composición de servicios en entornos diseñados
conforme al paradigma de la computación orientada a servicios.
Aunque un proceso de negocio no deja de ser un programa de
ordenador, la principal característica que lo diferencia
de los programas convencionales es su muy alto nivel de abstracción.
Este nivel de abstracción permite que el desarrollo,
implantación o modificación de procesos sea considerablemente más
ágil que en el caso de programas convencionales. Por otra parte,
aporta una gran flexibilidad durante la ejecución de los
mismos. Sin embargo, a pesar de este nivel de abstracción, también
las definiciones de procesos de negocio son susceptibles de
tener errores, especialmente debido al alto grado de concurrencia,
computación distribuida y dependencia de entidades externas
que las caracterizan.
Esto hace necesario el uso de técnicas de verificación que permitan
comprobar que el comportamiento de los procesos sea conforme a
sus especificaciones.
En esta tesis doctoral se realizan aportaciones en el ámbito
de la verificación de requisitos funcionales de procesos
de negocio. Por una parte, se propone una arquitectura
abierta, modular y extensible para la verificación de
procesos, que permite la integración de distintos lenguajes
de definición de procesos y herramientas de verificación,
y se basa en un sistema formal intermedio.
Por otra parte, se define este sistema formal intermedio,
llamado Modelo Formal Común (CFM),
que se basa en sistemas de estado--transición etiquetados, pero con
una notación y abstracciones orientadas a la
representación de procesos de negocio.
Con el objetivo de comprobar la expresividad y adecuación
de este formalismo para la representación de los mismos,
se realiza un análisis basado en patrones de workflow.
Adicionalmente, se integra BPEL4WS, un lenguaje
de definición de composiciones de servicios Web basado en procesos,
en la arquitectura.
Para ello, se define su semántica en términos del formalismo, así como
una metodología de transformación de definiciones de procesos
BPEL4WS a definiciones CFM.
También se integran en la arquitectura dos herramientas de verificación:
los model checkers Spin y NuSMV. Para ello, se define una
transformación entre definiciones CFM y los lenguajes de entrada
de estas herramientas.
|
