Semántica de simulación para relaciones de conformidad

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...