Semántica de simulación para relaciones de conformidad

Abstract

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

This thesis is about conformance relations you might set up between any two given systems, namely specification and implementation. As a novelty it introduces coinductive techniques to define iocos, a conformance relation enabled to track local context of process execution. iocos relying at the core a of a new Model Based Testing (MBT) Theory, a formal description of the systems is required; this is accomplished, firstly, by means of labeled transition systems and then using a more abstract approach, a process algebra. Testing theories are designed to state conformance relations by running a set of tests on an system –the implementation–, whose internal details are unknown. In particular, benefits of a MBT approach are immediate, since test generation can be achieved systematically provided a formal model of the specification, hence avoiding error-prone human factor; this is achieved by giving a test-generator algorithm accepting an specification as input, and yielding a set of tests, possibly infinite, large enough to state the conformance. Such an initial approach, testing offline, is improved to avoid waste of time and space in the form of testing online, where both test generation and execution steps are interleaved...