Generación de casos de prueba para composiciones de servicios web

En los últimos años se ha detectado un importante y sostenido aumento en la inversión que las empresas dedican al desarrollo de software basado en servicios (SOAs). El desarrollo de SOAs y, especialmente, los procesos de prueba de este tipo de software plantean un reto a los ingenieros que algunos autores califican como un cambio de paradigma en la ingeniería del software. Entre los retos que deben afrontarse en los procesos de prueba cabe destacar, por ejemplo, la falta de información homogénea acerca de los servicios disponibles y el coste asociado a la ejecución de SOAs. Una parte muy importante de los SOAs existentes hoy en día son composiciones de servicios y, concretamente, aquellas especificadas utilizando el estándar BPEL, que se ha convertido en un estándar de facto. En esta tesis se describe un método sistemático de generación de casos de prueba para composiciones de servicios especificadas en el lenguaje BPEL. Se utiliza el comprobador de modelos SPIN para generar automáticamente las especificaciones de los casos. Inicialmente se expone cómo obtener un modelo de comportamiento operacional expresado en el lenguaje PROMELA (el lenguaje de entrada de SPIN) a partir de la especificación de una composición de servicios expresada en BPEL. A continuación en el método se aplica un criterio de suficiencia dado, lo que se traduce en la instrumentación del modelo PROMELA y la obtención sistemática de un conjunto de requisitos de prueba. En la tesis se utilizan dos criterios de suficiencia diferentes basados en transiciones: cobertura de transiciones y cobertura de pares de transiciones adyacentes. Cada uno de los requisitos se transforma en una propiedad en lógica temporal LTL que se incluye como entrada de la herramienta SPIN. Al ejecutar el comprobador de modelos, se obtendrá un contraejemplo que cumple, al menos, el requisito incluido en la fórmula y que se transforma en un caso de prueba. Para ilustrar y validar el método, se incluyen (...