Tecnología UniTESK

La versión actual de la página aún no ha sido revisada por colaboradores experimentados y puede diferir significativamente de la versión revisada el 22 de diciembre de 2020; la verificación requiere 1 edición .

UniTESK (Unified Testing & Specification ToolKit) es una tecnología para probar software y hardware basada en especificaciones formales , desarrollada en el Instituto de Programación de Sistemas de la Academia Rusa de Ciencias . La tecnología es una combinación de técnicas bien establecidas que se pueden aplicar en varias combinaciones, combinándose y reforzándose mutuamente. Esto hace que la tecnología sea flexible y personalizable para los procesos de desarrollo existentes en todas las etapas del ciclo de vida del desarrollo de software, desde la recopilación y el análisis de requisitos hasta el mantenimiento.

La base para emitir veredictos sobre la corrección del comportamiento del sistema bajo prueba son las especificaciones del contrato en forma de condiciones previas y posteriores , escritas en extensiones de lenguajes de programación tradicionales como C , Java , y que permiten hacer un veredicto completamente automático. Las especificaciones son una representación de los requisitos funcionales de un sistema. La forma de las especificaciones y los criterios de cobertura basados en ellas aseguran la trazabilidad de los requisitos .

Usadas con éxito en la práctica, las técnicas para construir pruebas basadas en el recorrido de gráficos de estado pueden minimizar significativamente la cantidad de código de programa creado manualmente , mientras que al mismo tiempo aseguran la diversidad y la masividad del conjunto de prueba.

Las técnicas de abstracción de datos y los criterios de cobertura basados en requisitos permiten un control flexible sobre el tamaño del conjunto de prueba y la generación directa para cubrir requisitos específicos, lo que minimiza el tiempo de ejecución del conjunto de prueba.

Una capa intermedia especial disponible en la tecnología le permite personalizar rápidamente el conjunto de pruebas para diferentes implementaciones con la misma funcionalidad.

Todas estas técnicas proporcionan pruebas de alta calidad, trazabilidad de los requisitos y un alto nivel de reutilización de los componentes del conjunto de pruebas con un mínimo de trabajo manual y un tiempo de ejecución de prueba aceptable.

Pasos tecnológicos

Definición de la parte del sistema bajo prueba En este paso se determina la funcionalidad probada, es decir, parte de las capacidades del sistema bajo consideración que necesita ser probada, y la interfaz probada, es decir, la forma de acceder a las capacidades probadas. Definición y análisis de requisitos para el sistema bajo prueba Con base en el análisis de todos los datos de entrada, la comunicación con el cliente, los expertos y los usuarios, se identifican y sistematizan los requisitos para el sistema bajo prueba. Que se presentan además en forma de un modelo formal. Definición y análisis de requisitos para la integridad de las pruebas Se destacan criterios de exhaustividad de las pruebas, que se reflejan en el modelo formal. Desarrollo de pruebas Desarrollo de fuentes de datos de prueba y modelo de prueba en general.
Técnicas Básicas .
Enumeración de conjuntos finitos, enumeración de combinaciones, enumeración de valores límite y cercanos a ellos, enumeración de valores nodales y cercanos, enumeración de estructuras gramaticales usando generadores modulares, enumeración con filtrado, enumeración de gráficos y secuencias atribuidas.
Autómatas finitos, sistemas de transición etiquetados, representación implícita de modelos de autómatas, pruebas capa por capa de modelos complejos. Desarrollar adaptadores que vinculen las pruebas a la implementación bajo prueba Depuración y ejecución de pruebas Análisis de los resultados de las pruebas

Historial de creación

En 1994, el Instituto de Programación de Sistemas de la Academia Rusa de Ciencias (ISP RAS) , en virtud de un contrato con Nortel Networks , desarrolló una metodología y un conjunto de herramientas para automatizar las pruebas de interfaz de programa de aplicación (API) . La primera aplicación práctica de la metodología fue el núcleo del sistema operativo en tiempo real.
Durante 1994-1999 ISP RAS creó e instaló varias versiones de la tecnología KVEST-1 en Nortel Networks.
En 1998-1999, se completó la creación de la tecnología KVEST-2.
En 2000, la tecnología KVEST se adaptó para su uso en proyectos C y C++ .
En 1999, ISP RAS comenzó a desarrollar una tecnología de verificación de nueva generación: UniTESK (Unified Testing & Specification ToolKit).

Aplicación en la práctica

La tecnología se ha aplicado con éxito en muchos proyectos. Más interesantes:

Verificación de Open Linux ( OLVER ) (desde 2005);
Pruebas de integración y componentes de facturación de VimpelCom (desde 2007);
Probar la implementación móvil del protocolo IPv6 (2002-2003, 2 años-hombre);
Pruebas de Object Broker (2000, 1 hombre-año);
Pruebas de componentes del Marco ATM (1999-2000, 6 años-hombre);
Prueba y rediseño del sistema de soporte de aplicaciones (1998-1999, 2 años-hombre);
Pruebas del núcleo del sistema operativo (1994-1997, 25 años-hombre).

Apoyo instrumental

CTESK es una herramienta de prueba de software implementada en lenguaje C.
CTESK Community Edition es una versión gratuita y completamente funcional de la herramienta CTESK para la plataforma Linux .
JavaTESK es una herramienta de prueba de software implementada en el lenguaje Java .
C++TESK es una herramienta para probar software implementado en lenguaje C++ , así como modelos de equipos digitales síncronos en lenguajes de descripción de hardware .
Pinery : diseñado para generar datos de prueba de una estructura compleja basada en descripciones en forma de gramáticas (tales descripciones incluyen, por ejemplo, BNF , expresiones regulares , DTD , etc.).
OTK (Optimizer Testing Kit) es una herramienta para probar sistemas de software que trabajan con datos que tienen una estructura compleja. El uso de OTK es más efectivo cuando se prueban compiladores u otros sistemas formales de procesamiento de texto. El énfasis principal en OTK está en construir una variedad de datos de prueba de entrada.
SynTESK (Syntax Testing Kit) es una herramienta para probar analizadores (parsers) de lenguajes formales. SynTESK le permite verificar el cumplimiento de la implementación del analizador y la especificación de un lenguaje formal dado, es decir, que el analizador reconoce este lenguaje formal en particular.
MicroTESK (Microprocessor Testing Kit) es una herramienta para el desarrollo automatizado de generadores de programas de prueba para microprocesadores y otros dispositivos programables.

Literatura

Kulyamin V. V. . Criterios de cobertura de prueba basados en la estructura de las especificaciones del contrato // Proceedings of ISP RAS, UniTESK Approach: Results and Perspectives. 14(1):89-107, 2008 [1]
Grinevich A. I. , Kulyamin V. V. , Markovtsev D. A. , Petrenko A. K. , Rubanov V. V. , Khoroshilov A. V. Uso de métodos formales para garantizar el cumplimiento de los estándares de software // Procedimientos de ISP RAS, Provisión de confiabilidad y compatibilidad de los sistemas Linux. 10:51-68, 2006 [2]
Burdonov I. B. , Kosachev A. S. , Kulyamin V. V. Algoritmos de recorrido de grafos dirigidos no redundantes: caso no determinista //Programación. 30(1):2-17, 2004 [3]
Burdonov I. B. , Kosachev A. S. , Kulyamin V. V. Uso de máquinas de estados finitos para probar programas //Programación. 26(2):61-73, 2000 [4]
Bourdonov I. , Kossatchev A. , Kuliamin V. y Petrenko A. . Arquitectura de la suite de pruebas UniTesK // Proc. de FME 2002. LNCS 2391, pp. 77-88, Springer-Verlag, 2002. ISBN 3-540-43928-5
Bourdonov IB , Demakov AV , Jarov AA , Kossatchev AS , Kuliamin VV , Petrenko AK y Zelenov SV . Extensión de la especificación Java para el desarrollo de pruebas automatizadas // Actas de PSI'2001. Novosibirsk, Rusia, 2-6 de julio de 2001. LNCS 2244:301-307, Springer-Verlag, 2001. ISBN 978-3-540-43075-9 [5] (enlace no disponible)
Bourdonov I. , Kossatchev A. , Petrenko A. y Galter D .. KVEST: Generación Automatizada de Suites de Pruebas a partir de Especificaciones Formales //FM'99: Métodos Formales. LNCS 1708, Springer-Verlag, 1999, págs. 608-621. ISBN 3-540-66587-0 [6] (enlace no disponible)