OpenCyber Academy
Engenharia · Capítulo 30 · Português
Código do curso: OCA-138Capítulo 30: OCA-138-C030

Capítulo 30 — Laboratório de verificação I

Ensino gratuito e aberto para quem deseja proteger pessoas e tecnologias. Não é preciso criar uma conta para estudar ou consultar as respostas.

Mapa da aula

Aula 30 publicada. Mapa, exemplo, EX059.

flowchart TD
  N0["30.1 A verificação como campanha"]
  N1["30.2 Tipos de teste"]
  N2["30.3 Reprodutibilidade"]
  N3["30.4 Testes reprovados"]
  N4["30.6 Atividade prática: Laboratório 11"]
  N5["Síntese do capítulo"]
  N0 --> N1 --> N2 --> N3 --> N4 --> N5
  N5 --> EX["Exemplo resolvido"]
  EX --> Q["Exercício EX059"]

Desenho lógico

flowchart LR
  N0["30.1 A verificação como campanha"]
  N1["30.2 Tipos de teste"]
  N2["30.3 Reprodutibilidade"]
  N3["30.4 Testes reprovados"]
  N4["30.6 Atividade prática: Laboratório 11"]
  N5["Síntese do capítulo"]
  N0 --> N1 --> N2 --> N3 --> N4 --> N5 --> Q["EX059"]

[30.1 A verificação como campanha]
    |
    v
[30.2 Tipos de teste]
    |
    v
[30.3 Reprodutibilidade]
    |
    v
[30.4 Testes reprovados]
    |
    v
[30.6 Atividade prática: Laboratório 11]
    |
    v
[Síntese do capítulo]
    |
    v
[Exemplo resolvido] --> [Exercício EX059]

Objetivos de aprendizagem e conexão

Ao fim deste capítulo você será capaz de (1) planejar e executar uma campanha de verificação de controles de segurança com critérios definidos de aprovação e reprovação; (2) usar testes baseados em exemplos, de limites, negativos e baseados em propriedades; (3) registrar os resultados para que outro engenheiro possa reproduzi-los; e (4) tratar testes reprovados com honestidade, incluindo o novo teste depois das correções. Ele verifica a implementação do Capítulo 28 e prepara o Capítulo 38 (validação) e o Capítulo 40 (Laboratório de verificação II).

30.1 A verificação como campanha

A verificação responde: a implementação atende à sua especificação? Um plano de campanha lista, para cada requisito, os casos de teste, o ambiente, as entradas, o procedimento, o resultado esperado, o critério de aprovação e quem o executa. Os testes são escritos antes da execução e não são alterados para fazer os resultados passarem. Os resultados incluem detalhes do ambiente (versões de software, sementes, configuração) para que o teste possa ser repetido. O plano de campanha do TMRP lista T1 a T7 contra R1 a R8, com critérios de aprovação fixados antes da execução de qualquer teste; R9 ainda não tem teste atribuído, o que o mapa de evidências expõe depois. Cada teste nomeia seu ambiente e quem o executa.

30.2 Tipos de teste

Os testes de exemplo mostram a presença do comportamento correto nos casos escolhidos; os testes baseados em propriedades e de injeção de falhas buscam de forma mais ampla a ausência de comportamento incorreto. Nenhum deles prova a correção para todas as entradas, exceto em domínios finitos pequenos (Capítulo 2).

30.3 Reprodutibilidade

Defina a semente de todo gerador aleatório e imprima-a; registre as versões das ferramentas e bibliotecas; guarde as entradas de teste; armazene os resultados com a revisão do código-fonte. Um teste reprovado que não pode ser reproduzido não pode ser corrigido nem verificado de novo. O registro do T3 do TMRP segue essa regra: ele informa a semente, o número de casos gerados e a versão do Python, para que qualquer pessoa possa executar de novo o teste baseado em propriedades e ver as mesmas trinta e uma aceitações de NaN na v1 e nenhuma na v2. Sem a semente, um revisor só poderia aceitar o resultado na confiança. O mesmo registro armazena a revisão do código-fonte de cada versão do validador.

30.4 Testes reprovados

Um teste reprovado é informação. Registre-o como reprovado, com evidências; analise a causa raiz; corrija; execute de novo o teste reprovado e o conjunto de regressão; registre o novo teste. Nunca rotule de novo uma reprovação como "não aplicável" porque o prazo está próximo (Capítulo 10). Se uma reprovação for aceita temporariamente, ela precisa de um controle compensatório, um dono e uma data. O T3 é o modelo: reprovado na v1, corrigido na v2, testado de novo e registrado. A reprovação da v1 nunca foi rotulada de novo, e o controle compensatório da PS4 tinha um dono e uma data.

30.5 Exemplo resolvido: T3, limites de setpoint (sintético)

O teste T3 verifica R3. Os testes de exemplo na v1 (dentro da faixa, acima, abaixo, passo grande) são aprovados. O teste baseado em propriedades gera 2.000 casos com a semente 30, um em cada dez sorteado entre valores especiais (NaN, ±∞, limites exatos). A v1 aceita 31 valores inseguros — todos NaN. A v2 não aceita nenhum. O T3 é registrado como reprovado na v1, com causa raiz "comparações negativas são falsas para NaN", corrigido na v2, testado de novo e aprovado na v2, com a semente e a versão do Python registradas. Os dois resultados permanecem no registro. O resultado do novo teste é depois lançado na matriz de rastreabilidade.

30.6 Atividade prática: Laboratório 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))

Saída esperada:

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

Os testes de exemplo dão as mesmas respostas para os dois validadores, então não conseguem distinguir a v1 da v2. É a execução baseada em propriedades que os separa: a v1 aceita trinta e um valores inseguros, todos NaN, enquanto a v2 não aceita nenhum. A semente trinta torna a execução repetível. Observe que o gerador sorteia valores especiais apenas uma vez em cada dez; sem isso, o NaN quase nunca apareceria e o bug ficaria escondido por mais casos aleatórios que fossem tentados. Registre a semente junto com o resultado.

30.7 Erros comuns e limites

O registro do T3 do TMRP evita cada um desses erros. Sua propriedade foi escrita antes da execução, seu gerador tem semente, a reprovação na v1 permaneceu registrada como reprovação, e o relatório alega apenas que nenhum valor inseguro foi encontrado entre os casos gerados, e não que a v2 está correta para todas as entradas. A semente e a versão ficam armazenadas com o resultado.

Exercícios — capítulo 30

EX059 — Conte as reprovações. Objetivo: raciocinar sobre testes gerados. Entradas: Laboratório 11. Passos: (1) explique por que todas as 31 aceitações inseguras são NaN; (2) estime quantos casos NaN o gerador produziu (um em cada dez casos é um valor especial, escolhido uniformemente entre cinco) e compare com 31; (3) explique por que nem todo caso NaN é uma aceitação insegura na v1 — ou mostre que todo NaN é aceito. Evidência esperada: raciocínio e números. Rubrica: 3 = ≈ 200 casos especiais × 1/5 ≈ 40 NaN esperados, 31 observados, compatível com a variação aleatória, e todo NaN é aceito pela v1, então 31 é a contagem de NaN; 2 = parcial; 1 = sem números; 0 = nada.

EX060 — Plano de verificação para R2. Objetivo: planejar testes para a rejeição de repetições. Entradas: R2 e Laboratório 8. Passos: escreva um plano de teste com pelo menos seis casos (incluindo o reinício de cada lado, o estouro ou o máximo do contador, a entrega fora de ordem), resultados esperados e critérios de aprovação. Evidência esperada: tabela. Rubrica: 3 = os casos cobrem o reinício e a ordenação, resultados esperados coerentes com o projeto da §19.5, critérios inequívocos; 2 = reinício ausente; 1 = apenas o caminho feliz; 0 = nada.

Síntese do capítulo

A verificação é uma campanha planejada, com critérios fixados com antecedência. Combine testes de exemplo, de limites, negativos, baseados em propriedades e de injeção de falhas; torne cada execução reprodutível; e trate as reprovações como informação a ser corrigida e verificada de novo, nunca rotulada de novo.

Respostas comentadas

EX059. O NaN dá falso em qualquer comparação, então as verificações negativas da v1 nunca o rejeitam, enquanto ±∞ falham em > hi ou < lo. Cerca de 2.000/10 = 200 casos de valores especiais, um quinto deles NaN → cerca de 40 esperados; 31 observados (o gerador sorteou 31 casos NaN com a semente 30), bem dentro da variação aleatória (desvio-padrão binomial ≈ 5,7). Todo caso NaN é uma aceitação insegura pela v1, então as 31 reprovações são exatamente os casos NaN.

EX060. Casos: (1) contadores 1, 2, 3 → todos aceitos; (2) repetir o 2 → rejeitado; (3) contador menor → rejeitado; (4) reinício do receptor e depois repetição de uma mensagem antiga → rejeitada (exige estado persistido ou rotação de chaves); (5) reinício do emissor → retoma em persistido + 1.000, aceito; contadores antigos rejeitados; (6) entrega fora de ordem (3 antes de 2) → 3 aceito, 2 rejeitado e registrado em log (comportamento documentado); (7) contador no máximo 2⁶⁴ − 1 → rotação de chaves exigida antes do estouro; testar que o emissor se recusa a dar a volta. Critérios de aprovação: resultados exatos de aceitação/rejeição e entradas de log.