Semántica de simulación para relaciones de conformidad

Resumen

Esta tesis trata de las llamadas relaciones de conformidad que pueden darse entre dos sistemas cualesquiera, especificación e implementación. Como novedad introduce el uso de técnicas coinductivas para la definición de iocos, una relación de conformidad capaz de distinguir el contexto local de ejecución de un proceso. Al constituir iocos la parte central de una nueva teoría de Model Based Testing (MBT), se precisa de una descripción formal de los sistemas en juego; esto se lleva a cabo en primera instancia mediante sistemas de transiciones etiquetadas y posteriormente mediante un enfoque más abstracto, un álgebra de procesos. Las teorías de testing tienen por objeto confirmar las relaciones de conformidad mediante la ejecución de un conjunto de tests sobre un sistema --la implementación¿cuya estructura interna se desconoce. Particularmente los beneficios de un enfoque MBT son inmediatos, ya que la generación de los tests puede abordarse de manera sistemática una vez se disponga de un modelo formal de la especificación, lo que contribuye a eliminar el error imputable al factor humano; esto se logra dando un algoritmo generador de tests que toma cono entrada una especificación y produce un conjunto de tests, posiblemente infinito, suficientemente representativo para asegurar la relación de conformidad. Este enfoque inicial, conocido como testing offline o testing estático, es mejorado para ganar en eficiencia evitando un alto consumo en recursos tanto de tiempo como de memoria mediante la técnica de testing online o testing dinámico, donde ambos pasos de generación y ejecución se ejecutan de manera alternada. La Algoritmia también desempeña un papel importante cuando los modelos de la implementación son disponibles. Basándose en resultados clásicos del procesamiento de grafos, se propone una variante del Generalized Coarsest Partition Problem, GCPP, o Problema Generalizado de la Partición más Grande. El planteamiento que subyace a todo ello es simple: adoptando una estrategia de reducción, iocos es redefinida en un nuevo entorno bajo unas condiciones que pueden ser computadas eficientemente por el problema GCPP. Como resultado, se dispone una implementación ejecutable integrada en el marco de la conocida plataforma mCRL. También se exponen algunas estadísticas obtenidas a partir de experimentos con casos de estudios de gran tamaño. Por último, se proporciona un cálculo correcto y completo al objeto de deducir la conformidad a partir de algunos resultados conocidos. Para lograrlo, es menester definir un sencillo lenguaje de procesos cuya congruencia con respecto a iocos es contrastada. Las pruebas pertinentes de corrección y completitud se proporcionan en primer lugar para reglas y fórmulas que contienen procesos finitos; en base a sucesivas aproximaciones finitas se lleva a cabo la corrección de la parte del cálculo que considera procesos infinitos.