
En informática , las pruebas basadas en modelos son un enfoque que aprovecha el diseño basado en modelos para diseñar y, posiblemente, ejecutar pruebas. Como se muestra en el diagrama de la derecha, un modelo puede representar el comportamiento deseado de un sistema bajo prueba (SUT). O bien, un modelo puede representar estrategias y entornos de prueba.
Un modelo que describe un SUT suele ser una presentación abstracta y parcial del comportamiento deseado del SUT. Los casos de prueba derivados de dicho modelo son pruebas funcionales al mismo nivel de abstracción que el modelo. Estos casos de prueba se conocen colectivamente como un conjunto de pruebas abstracto . Un conjunto de pruebas abstracto no se puede ejecutar directamente contra un SUT porque el conjunto está en un nivel de abstracción incorrecto. Un conjunto de pruebas ejecutable debe derivarse de un conjunto de pruebas abstracto correspondiente. El conjunto de pruebas ejecutable puede comunicarse directamente con el sistema bajo prueba. Esto se logra mapeando los casos de prueba abstractos a casos de prueba concretos adecuados para la ejecución. En algunos entornos de prueba basados en modelos, los modelos contienen suficiente información para generar conjuntos de pruebas ejecutables directamente. En otros, los elementos del conjunto de pruebas abstracto deben mapearse a instrucciones o llamadas a métodos específicos en el software para crear un conjunto de pruebas concreto. Esto se denomina resolver el "problema de mapeo". [ 1 ] En el caso de las pruebas en línea (véase más adelante), los conjuntos de pruebas abstractos existen solo conceptualmente, pero no como artefactos explícitos.
Las pruebas pueden derivarse de los modelos de diversas maneras. Dado que las pruebas suelen ser experimentales y se basan en heurísticas, no existe un único método óptimo conocido para su derivación. Es común consolidar todos los parámetros relacionados con la derivación de pruebas en un conjunto que a menudo se denomina "requisitos de prueba", "objetivo de la prueba" o incluso "caso(s) de uso". Este conjunto puede contener información sobre las partes del modelo en las que se debe centrar la atención o las condiciones para finalizar las pruebas (criterios de parada).
Dado que los conjuntos de pruebas se derivan de modelos y no del código fuente, las pruebas basadas en modelos suelen considerarse una forma de pruebas de caja negra .
Modelos
Especialmente en la ingeniería dirigida por modelos y la arquitectura dirigida por modelos , estos se construyen antes o en paralelo con los sistemas correspondientes. Los modelos también pueden construirse a partir de sistemas completos. Los lenguajes de modelado típicos para la generación de pruebas incluyen UML , SysML , lenguajes de programación convencionales, notaciones de máquinas finitas y formalismos matemáticos como Z , B ( Event-B ), Alloy o Rocq .
Implementación de pruebas basadas en modelos

Existen varias formas conocidas de implementar pruebas basadas en modelos, que incluyen pruebas en línea , generación fuera de línea de pruebas ejecutables y generación fuera de línea de pruebas implementables manualmente . [ 2 ]
Las pruebas en línea implican que una herramienta de prueba basada en modelos se conecta directamente al sistema bajo prueba (SUT) y lo prueba de forma dinámica.
La generación offline de pruebas ejecutables significa que una herramienta de pruebas basada en modelos genera casos de prueba como recursos legibles por ordenador que posteriormente pueden ejecutarse automáticamente; por ejemplo, una colección de clases de Python que incorpora la lógica de prueba generada.
La generación offline de pruebas que se pueden implementar manualmente significa que una herramienta de pruebas basada en modelos genera casos de prueba como recursos legibles por humanos que posteriormente pueden ayudar en las pruebas manuales; por ejemplo, un documento PDF en un idioma humano que describe los pasos de prueba generados.
Derivación algorítmica de pruebas
La eficacia de las pruebas basadas en modelos se debe principalmente al potencial de automatización que ofrecen. Si un modelo es legible por máquina y formal hasta el punto de tener una interpretación de comportamiento bien definida, los casos de prueba pueden, en principio, derivarse mecánicamente.
De máquinas de estados finitos
A menudo, el modelo se traduce o interpreta como un autómata de estados finitos o un sistema de transición de estados . Este autómata representa las posibles configuraciones del sistema bajo prueba. Para encontrar casos de prueba, se buscan rutas ejecutables en el autómata. Una ruta de ejecución posible puede servir como caso de prueba. Este método funciona si el modelo es determinista o puede transformarse en uno. Se pueden obtener valiosos casos de prueba no nominales aprovechando las transiciones no especificadas en estos modelos.
Dependiendo de la complejidad del sistema bajo prueba y del modelo correspondiente, el número de rutas puede ser muy grande, debido a la enorme cantidad de configuraciones posibles del sistema. Para encontrar casos de prueba que puedan cubrir un número apropiado, pero finito, de rutas, se necesitan criterios de prueba que guíen la selección. Esta técnica fue propuesta por primera vez por Offutt y Abdurazik en el artículo que dio inicio a las pruebas basadas en modelos. [ 3 ] Se han desarrollado múltiples técnicas para la generación de casos de prueba y Rushby las analiza. [ 4 ] Los criterios de prueba se describen en términos de grafos generales en el libro de texto de pruebas. [ 1 ]
Demostración de teoremas
La demostración de teoremas se utilizó originalmente para la demostración automatizada de fórmulas lógicas. Para los enfoques de prueba basados en modelos, el sistema se modela mediante un conjunto de predicados que especifican el comportamiento del sistema. [ 5 ] Para derivar casos de prueba, el modelo se divide en clases de equivalencia sobre la interpretación válida del conjunto de predicados que describen el sistema bajo prueba. Cada clase describe un comportamiento determinado del sistema y, por lo tanto, puede servir como caso de prueba. La partición más simple es con el enfoque de forma normal disyuntiva, en el que las expresiones lógicas que describen el comportamiento del sistema se transforman en la forma normal disyuntiva .
Programación lógica con restricciones y ejecución simbólica
La programación con restricciones permite seleccionar casos de prueba que satisfacen restricciones específicas mediante la resolución de un conjunto de restricciones sobre un conjunto de variables. El sistema se describe mediante restricciones. [ 6 ] La resolución del conjunto de restricciones puede realizarse mediante solucionadores booleanos (por ejemplo, solucionadores SAT basados en el problema de satisfacibilidad booleana ) o mediante análisis numérico , como la eliminación gaussiana . Una solución obtenida al resolver las fórmulas del conjunto de restricciones puede servir como caso de prueba para el sistema correspondiente.
La programación con restricciones se puede combinar con la ejecución simbólica. En este enfoque, un modelo de sistema se ejecuta simbólicamente, es decir, se recopilan restricciones de datos sobre diferentes rutas de control, y luego se utiliza el método de programación con restricciones para resolver las restricciones y generar casos de prueba. [ 7 ]
Verificación de modelos
Los verificadores de modelos también pueden utilizarse para la generación de casos de prueba. [ 8 ] Originalmente, la verificación de modelos se desarrolló como una técnica para comprobar si una propiedad de una especificación es válida en un modelo. Al utilizarse para realizar pruebas, se proporciona al verificador de modelos un modelo del sistema bajo prueba y una propiedad a probar. Dentro del procedimiento de verificación, si esta propiedad es válida en el modelo, el verificador de modelos detecta testigos y contraejemplos. Un testigo es una ruta donde se satisface la propiedad, mientras que un contraejemplo es una ruta en la ejecución del modelo donde se viola la propiedad. Estas rutas pueden utilizarse nuevamente como casos de prueba.
Generación de casos de prueba mediante un modelo de prueba de cadena de Markov
Las cadenas de Markov son una forma eficiente de gestionar las pruebas basadas en modelos. Los modelos de prueba realizados con cadenas de Markov pueden entenderse como un modelo de uso: se denominan pruebas basadas en modelos de uso/estadísticos. Los modelos de uso, es decir, las cadenas de Markov, se componen principalmente de dos artefactos : la máquina de estados finitos (FSM), que representa todos los posibles escenarios de uso del sistema probado, y los perfiles operativos (OP), que califican la FSM para representar estadísticamente cómo se utiliza o se utilizará el sistema. La primera (FSM) ayuda a saber qué se puede probar o se ha probado, y la segunda (OP) ayuda a derivar casos de prueba operativos. Las pruebas basadas en modelos de uso/estadísticos parten de la premisa de que no es posible probar exhaustivamente un sistema y que las fallas pueden ocurrir con una frecuencia muy baja. [ 9 ] Este enfoque ofrece una forma pragmática de derivar estáticamente casos de prueba centrados en mejorar la fiabilidad del sistema bajo prueba. Recientemente, las pruebas basadas en modelos de uso/estadísticos se han extendido para aplicarse a sistemas de software embebido. [ 10 ] [ 11 ]
Véase también
Referencias
- 1 2 Paul Ammann y Jeff Offutt. Introducción a las pruebas de software, 2.ª edición. Cambridge University Press, 2016.
- ↑ Pruebas prácticas basadas en modelos: un enfoque de herramientas. Archivado el 25/08/2012 en Wayback Machine , Mark Utting y Bruno Legeard, ISBN 978-0-12-372501-1Morgan-Kaufmann 2007
- ↑ Jeff Offutt y Aynur Abdurazik. Generación de pruebas a partir de especificaciones UML. Segunda Conferencia Internacional sobre el Lenguaje Unificado de Modelado (UML '99), páginas 416-429, Fort Collins, CO, octubre de 1999.
- ↑ John Rushby. Generación automatizada de pruebas y software verificado. Software verificado: teorías, herramientas, experimentos: Primera conferencia IFIP TC 2/WG 2.3, VSTTE 2005, Zúrich, Suiza, 10-13 de octubre. págs. 161-172, Springer-Verlag
- ↑ Brucker, Achim D.; Wolff, Burkhart (2012). "Sobre las pruebas basadas en demostradores de teoremas" . Aspectos formales de la computación . 25 (5): 683– 721. CiteSeerX 10.1.1.208.3135 . doi : 10.1007/s00165-012-0222-y . S2CID 5774837 .
- ↑ Jefferson Offutt. Generación automática de datos de prueba basada en restricciones. IEEE Transactions on Software Engineering, 17:900-910, 1991
- ↑ Antti Huima. Implementación de Conformiq Qtronic. Pruebas de software y sistemas de comunicación, Lecture Notes in Computer Science, 2007, Volumen 4581/2007, 1-12, DOI: 10.1007/978-3-540-73066-8_1
- ↑ Gordon Fraser, Franz Wotawa y Paul E. Ammann. Pruebas con verificadores de modelos: una revisión. Software Testing, Verification and Reliability, 19(3):215–261, 2009. URL:
- ↑ Hélène Le Guen. Validation d'un logiciel par le test statistique d'usage : de la modelisation de la decision à la livraison, 2005. URL: ftp://ftp.irisa.fr/techreports/theses/2005/leguen.pdf
- ↑ Böhr, Frank (2011). "Pruebas estadísticas basadas en modelos de sistemas embebidos". Cuarta Conferencia Internacional IEEE de 2011 sobre Talleres de Pruebas, Verificación y Validación de Software . pp. 18–25 . doi : 10.1109/ICSTW.2011.11 . ISBN 978-1-4577-0019-4. S2CID 9582606 .
- ↑ Böhr, Frank (2012). Pruebas estadísticas basadas en modelos de software embebido en tiempo real con señales continuas y discretas en un entorno concurrente: El enfoque de la red de uso . Verlag Dr. Hut. ISBN 978-3843903486.
Lecturas adicionales
- Perfil de prueba UML 2 de OMG;
- Bringmann, E.; Krämer, A. (2008). «Conferencia Internacional de 2008 sobre Pruebas, Verificación y Validación de Software». Conferencia Internacional de 2008 sobre Pruebas, Verificación y Validación de Software (ICST). pp. 485–493 . CiteSeerX 10.1.1.729.8107 . doi : 10.1109/ICST.2008.45 . ISBN 978-0-7695-3127-4.
- Pruebas prácticas basadas en modelos: un enfoque de herramientas , Mark Utting y Bruno Legeard, ISBN 978-0-12-372501-1Morgan-Kaufmann 2007.
- Análisis y pruebas de software basadas en modelos con C# , Jonathan Jacky, Margus Veanes, Colin Campbell y Wolfram Schulte, ISBN 978-0-521-68761-4, Cambridge University Press 2008.
- Pruebas basadas en modelos de sistemas reactivos. Serie de conferencias avanzadas, LNCS 3472, Springer-Verlag, 2005. ISBN 978-3-540-26278-7.
- Hong Zhu et al. (2008). AST '08: Actas del 3er Taller Internacional sobre Automatización de Pruebas de Software . ACM Press. ISBN 978-1-60558-030-2.
- Santos-Neto, P.; Resende, R.; Pádua, C. (2007). «Actas del simposio ACM de 2007 sobre computación aplicada - SAC '07». Actas del simposio ACM de 2007 sobre computación aplicada - SAC '07 . Simposio sobre computación aplicada . pp. 1409–1415 . doi : 10.1145/1244002.1244306 . ISBN 978-1-59593-480-2.
- Roodenrijs, E. (Primavera de 2010). "Las pruebas basadas en modelos añaden valor" . Methods & Tools . 18 (1): 33– 39. ISSN 1661-402X .
- Revisión sistemática del soporte de herramientas de prueba basadas en modelos , Muhammad Shafique, Yvan Labiche, Universidad de Carleton, Informe técnico, mayo de 2010.
- Zander, Justyna; Schieferdecker, Ina; Mosterman, Pieter J. , eds. (2011). Pruebas basadas en modelos para sistemas embebidos . Análisis computacional, síntesis y diseño de sistemas dinámicos. Vol. 13. Boca Raton: CRC Press . ISBN 978-1-4398-1845-9.
- Encuesta de usuarios sobre pruebas basadas en modelos 2011/2012: Resultados y análisis. Robert V. Binder. System Verification Associates, febrero de 2012.
- Pruebas de software