PICKLES: a Natural Language Framework for Requirement Specification and Model-Based Testing

A continuación se presenta un resumen técnico detallado del artículo "PICKLES: un marco de lenguaje natural para la especificación de requisitos y las pruebas basadas en modelos".

1. Enunciado del Problema

El artículo aborda una tensión crítica en las pruebas de software industrial, particularmente para sistemas críticos para la seguridad:

• La limitación de las Pruebas Basadas en Modelos (MBT): Aunque MBT ofrece pruebas rigurosas, sistemáticas y de alta cobertura mediante modelos formales, su adopción se ve obstaculizada por la dificultad de definir y mantener dichos modelos. A menudo requieren experiencia especializada, carecen de legibilidad para las partes interesadas no técnicas y crean barreras de comunicación.
• La limitación del Desarrollo Guiado por el Comportamiento (BDD): BDD utiliza escenarios en lenguaje natural legibles por humanos (Dado-Cuando-Entonces) para facilitar la colaboración. Sin embargo, BDD se basa en ejemplos concretos, lo que a menudo conduce a:
  • Ambigüedad e Incompletitud: El lenguaje natural puede ser vago.
  • Baja Cobertura: La prueba de ejemplos aislados a menudo pasa por alto casos extremos y secuencias complejas de interacción.
  • Costos de Mantenimiento: Grandes suites de casos de prueba específicos son costosas de mantener y actualizar.

El Desafío Central: ¿Cómo lograr la precisión y la alta cobertura de MBT mientras se conservan los beneficios de accesibilidad, legibilidad y colaboración de las partes interesadas de BDD, sin obligar a los profesionales a elegir entre ambos?

2. Metodología: El Marco PICKLES

Los autores proponen PICKLES (Lenguaje Basado en Palabras Clave de Entrada y Flujo de Control Preciso para Escenarios de Prueba), un marco que une BDD y MBT mediante un pipeline de traducción bidireccional.

A. El Lenguaje Específico de Dominio (PicklesDSL)

Pickles extiende la sintaxis Gherkin estándar (Dado-Cuando-Entonces) con construcciones formales para eliminar la ambigüedad:

• Configuración de Variables: Un bloque de preludio donde las variables se tipifican explícitamente (por ejemplo, entero, booleano, array, estructura) y se les asignan dominios/rangos (por ejemplo, [1, 3], {AV, PART_AV}).
• Parametrización: Los pasos pueden hacer referencia a variables e incluir Bloques de Guardia (condiciones) utilizando operadores lógicos (Y, O) y cuantificadores (al menos, como máximo, exactamente).
• Estructura:
  • Dado: Define precondiciones y guardias de estado inicial.
  • Cuando: Define interacciones de entrada con parámetros y guardias.
  • Entonces: Define salidas esperadas y guardias de validación.

B. Semántica Formal: Sistemas de Transición Simbólica (STS)

El marco traduce las especificaciones PicklesDSL a Sistemas de Transición Simbólica (STS), un formalismo que extiende los Sistemas de Transición Etiquetados con construcciones de datos.

• Traducción (Especificación $\to$ STS):
  • Cada escenario Pickles se mapea a un STS parcial.
  • Las cláusulas Dado se convierten en guardias iniciales.
  • Las cláusulas Cuando se convierten en conmutadores de entrada (transiciones).
  • Las cláusulas Entonces se convierten en conmutadores de salida.
  • Las variables y las guardias se mapean a parámetros de STS, variables de ubicación y predicados lógicos.
• Composición de Modelos:
  • Los STS de escenarios individuales se componen en un Modelo Maestro.
  • Composición de Elección ($\bowtie$): Fusiona los estados iniciales de múltiples escenarios, permitiendo que cualquier escenario comience.
  • Composición Secuencial ($\triangleright$): Conecta los estados sumidero (final) de un STS con los estados iniciales de otros, permitiendo la generación de trazas de ejecución largas que combinan múltiples escenarios.

C. Generación de Pruebas y Traducción Inversa

• Generación de Pruebas: Se aplican algoritmos estándar de MBT (específicamente orientados a lograr una cobertura del 100% de conmutadores) al Modelo Maestro para generar casos de prueba formales (secuencias de conmutadores con valores de parámetros específicos).
• Traducción Inversa (STS $\to$ Pickles): Los casos de prueba formales se traducen de nuevo a la sintaxis PicklesDSL.
  • Los valores de entrada se definen explícitamente en los pasos Cuando.
  • Los valores de salida se reemplazan por las guardias Entonces originales para validar el comportamiento del Sistema Bajo Prueba (SUT).
  • El resultado es un caso de prueba ejecutable y legible por humanos compatible con herramientas BDD estándar (por ejemplo, Cucumber).

3. Contribuciones Clave

1. PicklesDSL: Un nuevo Lenguaje Específico de Dominio que preserva la estructura Gherkin pero añade tipado explícito de variables, definiciones de dominio y restricciones de flujo de control, garantizando especificaciones inequívocas.
2. Traducción Bidireccional: Un mapeo formal entre PicklesDSL y Sistemas de Transición Simbólica (STS), que permite un movimiento fluido entre requisitos legibles por humanos y modelos formales.
3. Composición de Modelo Maestro: Un método para componer automáticamente STS parciales de escenarios individuales en un Modelo Maestro unificado, permitiendo el descubrimiento de errores de interacción complejos que los escenarios aislados pasan por alto.
4. Implementación de Prototipo: Una herramienta basada en Python (utilizando el analizador Lark) que automatiza los procesos de traducción, composición y traducción inversa.
5. Validación Industrial: Aplicación del marco a un componente real de gestión de tráfico de la empresa Technolution.

4. Resultados

El marco fue evaluado mediante un estudio de caso que involucraba un componente de un sistema de gestión de tráfico. Los resultados demostraron mejoras significativas sobre los enfoques BDD tradicionales utilizando el mismo conjunto de escenarios definidos manualmente:

• Cobertura de Transiciones:
  • BDD Tradicional: La ejecución de escenarios de forma aislada cubrió solo el ~30% de las transiciones del sistema posibles.
  • Pickles: Al componer escenarios y generar pruebas desde el Modelo Maestro, la cobertura aumentó al 100%. Esto representa una mejora de 70 puntos porcentuales.
• Cobertura de Entrada:
  • El BDD tradicional con valores codificados dura ejerce una fracción mínima de las entradas posibles.
  • Pickles, al utilizar dominios de variables y análisis de límites, representó 112 posibilidades de entrada distintas para un solo escenario (Escenario 02) que de otro modo requeriría cientos de casos de prueba manuales. El estudio notó una mejora del 98.5% en la cobertura de entrada en comparación con los ejemplos concretos de BDD.
• Eficiencia: Lograr una cobertura del 100% de transiciones manualmente habría requerido al menos siete trazas de prueba distintas. Pickles logró esto con solo cuatro escenarios de entrada, reduciendo significativamente el esfuerzo manual y los costos de mantenimiento.

5. Significado

El marco PICKLES representa un paso significativo hacia adelante en la accesibilidad de las Pruebas Basadas en Modelos para los profesionales industriales:

• Cerrando la Brecha: Elimina con éxito el compromiso entre legibilidad y precisión. Las partes interesadas pueden colaborar en los requisitos en lenguaje natural, mientras que el sistema garantiza automáticamente el rigor formal.
• Pruebas Desplazadas a la Izquierda: Al permitir la composición automática de escenarios, permite que las pruebas de integración y a nivel de sistema se realicen más temprano en el ciclo de vida del desarrollo, detectando errores de interacción que las pruebas unitarias aisladas pasan por alto.
• Mantenibilidad: Los cambios en los requisitos (por ejemplo, rangos de variables) se propagan automáticamente a todos los casos de prueba generados, reduciendo la carga de mantenimiento asociada con grandes suites BDD.
• Explicabilidad: A diferencia de los modelos formales de caja negra, los casos de prueba generados permanecen en formato Pickles legible por humanos, lo que facilita explicar los resultados de las pruebas a gerentes y auditores no técnicos.

En conclusión, PICKLES demuestra que al fundamentar las especificaciones en lenguaje natural en semántica formal y aprovechar la composición automática de modelos, las organizaciones pueden lograr la alta fiabilidad de MBT sin sacrificar los beneficios colaborativos de BDD.