OpenCyber Academy
Ingeniería · Capítulo 30 · Español
Código del curso: OCA-138Capítulo 30: OCA-138-C030

Capítulo 30 — Laboratorio de verificación I

Aprendizaje gratuito y abierto para quienes desean proteger a las personas y la tecnología. No se necesita una cuenta para estudiar ni consultar las respuestas.

Mapa de la lección

Lección 30 publicada. Mapa, ejemplo, EX059.

flowchart TD
  N0["Resultados de aprendizaje y conexión"]
  N1["30.1 La verificación como campaña"]
  N2["30.2 Tipos de prueba"]
  N3["30.3 Reproducibilidad"]
  N4["30.4 Pruebas fallidas"]
  N5["30.6 Actividad práctica: Lab 11"]
  N6["Síntesis del capítulo"]
  N0 --> N1 --> N2 --> N3 --> N4 --> N5 --> N6
  N6 --> EX["Ejemplo resuelto"]
  EX --> Q["Ejercicio EX059"]

Dibujo lógico

flowchart LR
  N0["Resultados de aprendizaje y conexión"]
  N1["30.1 La verificación como campaña"]
  N2["30.2 Tipos de prueba"]
  N3["30.3 Reproducibilidad"]
  N4["30.4 Pruebas fallidas"]
  N5["30.6 Actividad práctica: Lab 11"]
  N6["Síntesis del capítulo"]
  N0 --> N1 --> N2 --> N3 --> N4 --> N5 --> N6 --> Q["EX059"]
[Resultados de aprendizaje y conexión]
    |
    v
[30.1 La verificación como campaña]
    |
    v
[30.2 Tipos de prueba]
    |
    v
[30.3 Reproducibilidad]
    |
    v
[30.4 Pruebas fallidas]
    |
    v
[30.6 Actividad práctica: Lab 11]
    |
    v
[Síntesis del capítulo]
    |
    v
[Ejemplo resuelto] --> [Ejercicio EX059]

Resultados de aprendizaje y conexión

Al terminar este capítulo, usted podrá (1) planificar y ejecutar una campaña de verificación de controles de seguridad con criterios de aprobación y rechazo definidos; (2) usar pruebas basadas en ejemplos, de límites, negativas y basadas en propiedades; (3) registrar los resultados de modo que otro ingeniero pueda reproducirlos; y (4) tratar con honestidad las pruebas fallidas, incluida la repetición de la prueba tras las correcciones. Verifica la implementación del capítulo 28 y prepara el capítulo 38 (validación) y el capítulo 40 (Laboratorio de verificación II).

30.1 La verificación como campaña

La verificación responde a la pregunta: ¿cumple la implementación su especificación? Un plan de campaña enumera, para cada requisito, los casos de prueba, el entorno, las entradas, el procedimiento, el resultado esperado, el criterio de aprobación y quién la ejecuta. Las pruebas se escriben antes de la ejecución y no se modifican para que los resultados aprueben. Los resultados incluyen los detalles del entorno (versiones de software, semillas, configuración) para que la prueba pueda repetirse. El plan de campaña del TMRP enumera las pruebas T1 a T7 frente a R1 a R8, con criterios de aprobación fijados antes de ejecutar ninguna prueba; R9 aún no tiene prueba asignada, lo que el mapa de evidencias pone de manifiesto más adelante. Cada prueba indica su entorno y quién la ejecuta.

30.2 Tipos de prueba

Las pruebas basadas en ejemplos muestran la presencia de un comportamiento correcto en los casos elegidos; las pruebas basadas en propiedades y las de inyección de fallos buscan de forma más amplia la ausencia de comportamiento incorrecto. Ninguna demuestra la corrección para todas las entradas, salvo en dominios finitos pequeños (capítulo 2).

30.3 Reproducibilidad

Fije la semilla de todo generador aleatorio e imprímala; registre las versiones de herramientas y bibliotecas; conserve las entradas de prueba; almacene los resultados junto con la revisión del código fuente. Una prueba fallida que no puede reproducirse no puede corregirse ni volver a verificarse. El registro de T3 del TMRP sigue esta regla: indica la semilla, el número de casos generados y la versión de Python, de modo que cualquiera puede volver a ejecutar la prueba basada en propiedades y ver las mismas treinta y una aceptaciones de NaN en v1 y ninguna en v2. Sin la semilla, un revisor solo podría aceptar el resultado por confianza. El mismo registro almacena la revisión del código fuente de cada versión del validador.

30.4 Pruebas fallidas

Una prueba fallida es información. Regístrela como fallida, con evidencia; analice la causa raíz; corrija; vuelva a ejecutar la prueba fallida y el conjunto de regresión; registre la nueva prueba. Nunca vuelva a etiquetar un fallo como «no aplicable» porque se acerca el plazo (capítulo 10). Si un fallo se acepta temporalmente, necesita un control compensatorio, un responsable y una fecha. T3 es el modelo: falló en v1, se corrigió en v2, se volvió a probar y se registró. El fallo de v1 nunca se reetiquetó, y el control compensatorio PS4 tenía responsable y fecha.

30.5 Ejemplo resuelto: límites de consigna en T3 (sintético)

La prueba T3 verifica R3. Las pruebas basadas en ejemplos sobre v1 (dentro del rango, por encima, por debajo, paso grande) aprueban. La prueba basada en propiedades genera 2.000 casos con la semilla 30, uno de cada diez extraído de valores especiales (NaN, ±∞, límites exactos). v1 acepta 31 valores inseguros, todos NaN. v2 no acepta ninguno. T3 se registra como fallida en v1, con la causa raíz «las comparaciones negativas son falsas para NaN», se corrige en v2, se vuelve a probar y queda aprobada en v2, con la semilla y la versión de Python registradas.

Ambos resultados permanecen en el registro. El resultado de la nueva prueba se anota después en la matriz de trazabilidad.

30.6 Actividad práctica: Lab 11

# Lab 11 - property-based testing of a setpoint validator finds what example tests missed (offline)
import random, math
def validate_v1(new, old, lo=0.5, hi=5.5, max_step=0.5):
    if new < lo: return False
    if new > hi: return False
    if abs(new - old) > max_step: return False
    return True
def validate_v2(new, old, lo=0.5, hi=5.5, max_step=0.5):
    if not (isinstance(new, float) and math.isfinite(new)): return False
    return lo <= new <= hi and abs(new - old) <= max_step
examples = [(3.0, 3.2), (6.0, 5.8), (0.2, 0.6), (4.0, 3.0)]
print("example tests v1:", [validate_v1(n, o) for n, o in examples])
rng = random.Random(30)
specials = [float("nan"), float("inf"), -float("inf"), 5.5, 0.5]
def prop(f, trials=2000):
    fails = []
    for i in range(trials):
        old = rng.uniform(0.5, 5.5)
        new = rng.choice(specials) if i % 10 == 0 else rng.uniform(-1, 7)
        ok = f(new, old)
        safe = math.isfinite(new) and 0.5 <= new <= 5.5 and abs(new - old) <= 0.5
        if ok and not safe: fails.append(new)
    return fails
f1 = prop(validate_v1); f2 = prop(validate_v2)
print("v1 unsafe acceptances:", len(f1), "first:", f1[:1])
print("v2 unsafe acceptances:", len(f2))

Salida esperada:

example tests v1: [True, False, False, False]
v1 unsafe acceptances: 31 first: [nan]
v2 unsafe acceptances: 0

Las pruebas basadas en ejemplos dan las mismas respuestas para ambos validadores, de modo que no pueden distinguir v1 de v2. Lo que los separa es la ejecución basada en propiedades: v1 acepta treinta y un valores inseguros, todos NaN, mientras que v2 no acepta ninguno. La semilla treinta hace que la ejecución sea repetible. Observe que el generador extrae valores especiales solo una vez de cada diez; sin eso, NaN casi nunca aparecería y el error seguiría oculto por muchos casos aleatorios que se probaran. Registre la semilla junto con el resultado.

30.7 Errores comunes y límites

El registro de T3 del TMRP evita cada uno de estos errores. Su propiedad se escribió antes de la ejecución, su generador tiene semilla, el fallo en v1 siguió registrado como fallido y el informe afirma solo que no se encontró ningún valor inseguro entre los casos generados, no que v2 sea correcto para cualquier entrada. La semilla y la versión se almacenan con el resultado.

Ejercicios — capítulo 30

EX059 — Cuente los fallos. Objetivo: razonar sobre pruebas generadas. Entradas: Lab 11. Pasos: (1) explique por qué las 31 aceptaciones inseguras son NaN; (2) estime cuántos casos NaN produjo el generador (uno de cada diez casos es un valor especial, elegido de manera uniforme entre cinco) y compárelo con 31; (3) explique por qué no todo caso NaN es una aceptación insegura en v1, o demuestre que todo NaN se acepta. Evidencia esperada: razonamiento y cifras. Rúbrica: 3 = ≈ 200 casos especiales × 1/5 ≈ 40 NaN esperados, 31 observados, compatible con la variación aleatoria, y todo NaN es aceptado por v1, de modo que 31 es el número de NaN; 2 = parcial; 1 = sin cifras; 0 = nada.

EX060 — Plan de verificación para R2. Objetivo: planificar pruebas de rechazo de repeticiones. Entradas: R2 y el Lab 8. Pasos: redacte un plan de pruebas con al menos seis casos (incluido el reinicio de cada lado, el desbordamiento o el máximo del contador y la entrega fuera de orden), resultados esperados y criterios de aprobación. Evidencia esperada: tabla. Rúbrica: 3 = los casos cubren el reinicio y el orden, los resultados esperados son coherentes con el diseño del §19.5 y los criterios no son ambiguos; 2 = falta el reinicio; 1 = solo el camino feliz; 0 = nada.

Síntesis del capítulo

La verificación es una campaña planificada con criterios fijados de antemano. Combine pruebas basadas en ejemplos, de límites, negativas, basadas en propiedades y de inyección de fallos; haga reproducible cada ejecución; y trate los fallos como información que debe corregirse y volver a verificarse, nunca reetiquetarse.

Respuestas desarrolladas

EX059. NaN da falso en cualquier comparación, de modo que las comprobaciones negativas de v1 nunca lo rechazan, mientras que ±∞ fallan en > hi o en < lo. Unos 2.000/10 = 200 casos de valores especiales, una quinta parte NaN → unos 40 esperados; 31 observados (el generador extrajo 31 casos NaN con la semilla 30), dentro de la variación aleatoria (desviación típica binomial ≈ 5,7). Todo caso NaN es una aceptación insegura de v1, así que los 31 fallos son exactamente los casos NaN.

EX060. Casos: (1) contadores 1, 2, 3 → todos aceptados; (2) repetición de 2 → rechazado; (3) contador inferior → rechazado; (4) reinicio del receptor y luego repetición de un mensaje antiguo → rechazado (requiere estado persistido o rotación de claves); (5) reinicio del emisor → reanuda en el valor persistido + 1.000, aceptado; contadores antiguos rechazados; (6) entrega fuera de orden (3 antes que 2) → 3 aceptado, 2 rechazado y registrado (comportamiento documentado); (7) contador en el máximo 2⁶⁴ − 1 → se requiere rotación de claves antes del desbordamiento; pruebe que el emisor se niega a desbordar. Criterios de aprobación: resultados exactos de aceptación o rechazo y entradas de registro.