Contribución a la fase de prueba de sistemas concurrentes y distribuidos mediante técnicas de descripción formal

Resumen

El objetivo de esta tesis es analizar y formalizar nuevas tecnicas para mejorar a fase de pruebas de sistemas distribuidos modelados mediante formalismos de caja gris, Las aportaciones realizadas adaptan la teoria clasica al marco distribuido proporcionando tecncias para la obtencion de pruebas que eviten los problemas de complejidad, explosion de estados y baja reutilizacion que aparecen al modelar el sistema distribuido de forma global y centralizada. En primer lugar se introduce un formalismo de caja gris, que parte de los sistemas de transiciones etiquetados clasicos, pero que permite identificar los componentes que participan en las acciones del sistema. A partir de dicho formalismo se establecen relaciones de implementacion para medir, bajo distintas perspectivas, si las implementaciones de dichos componentes conforman a sus especificaciones respectivas. Posteriormente, se presenta el algoritmo GEPCG para la obtencion de especificaciones parciales, de los componentes del sistema, que posean comportamientos relacionados con las partes que se desean probar. Dichas descripciones parciales se pueden combinar posteriormente para describir concurrentemente el comportamiento del sistema relacionado con las partes de interes. Esto facilita el analisis modular del sistema sin la necesidad de hacer una composicion global previa. A continuacion se introduce el algoritmo del Muelle, que a partir de una traza de un componente y sin componer la especificacion global, proporciona trazas globales que permitan la ejecucion de dicha traza sobre el sistema. Este algoritmo tiene especial interes en las pruebas de diagnostico en las que se desea conocer ciertos comportamientos puntuales. El siguiente paso aborda la fase de generacion de casos y colecciones de pruebas. Se presentan diversos algoritmos que permiten la generacion de casos de prueba adaptados a los resultados que proporcionan los algoritmos GEPCG y del Muelle. A continuacion se in