Resumen:
La validación de la implementación de un sistema a través del testing es un
paso importante en la realización de sistemas complejos. Incluso la
verificación más cautelosa de una especificación no puede garantizar la
ausencia de errores en el proceso de implementación. Dada la especificación
S de un sistema según algún modelo formal y una implementación I de caja
negra (aquella que sólo puede ser vista en términos de sus datos de entrada
y salida sin el conocimiento de cómo trabaja internamente), intentamos
derivar a partir de S secuencias de datos de entrada que nos permitan
determinar a partir de los datos de salida que generan en I si I se ajusta a
S. Dichas secuencias pueden permitir (i) predecir el comportamiento de los
datos de salida, y en el caso de un comportamiento erróneo, (ii) encontrar
la causa de dicho error.
Varios modelos han sido utilizados para especificar sistemas de caja negra,
entre ellos Automatas de Entrada/Salida, Automatas de Entrada/Salida con
multi-puertos, Automatas de Entrada/Salida con ordenes parciales, etc. Si
bien estos formalismos permiten modelar la concurrencia del sistema, siguen
siendo modelos secuenciales y heredan muchas de sus limitaciones. Por lo
tanto, debemos abandonar el modelo de máquinas finitas y desarrollar un
nuevo modelo para el testing de sistemas de entrada/salida implementados
como caja negra.
En este trabajo presentamos una extensión de las Redes de Petri, un modelo
que permite la representación de sistemas distribuidos y discretos. Gracias
a este nuevo modelo hemos sido capaces de establecer una relación de
implementación y diseñar un algoritmo para testearla.
Director: Stefan Harr (LSV, École Normale Supérieure de Cachan - Francia)