Un marco de pruebas formal para comportamientos de diagramas de estado UML: de la teoría a la verificación automática

Proponemos un marco de pruebas formal para un subconjunto comportamental de diagramas de estado UML (UMLSDs). Se define una semántica operacional formal, que utiliza la misma semántica básica introducida en Latella et al. (1999), pero que está mejor adaptada a la teoría de pruebas. La nueva semántica se prueba consistente con nuestra semántica original y se garantiza que genera únicamente máquinas de estados finitos. Se definen preórdenes y equivalencias de pruebas adecuados que nos permiten igualar/distinguir sistemas en función de su interacción con el entorno circundante, abstraciendo su estructura interna. Finalmente, proporcionamos una forma de verificación automática efectiva de la equivalencia de pruebas de nuestros diagramas de estado, basada en técnicas y herramientas existentes.