Casos de aseguramiento

Un caso de aseguramiento es el argumento de su equipo de que un sistema es lo bastante bueno para un uso declarado. Recoge cada afirmación, el uso para el que se hace y la evidencia en que se apoya. El caso vive junto a la política de publicación, en assurance.yaml, así que se revisa en pull requests, y Oloproof lee cada afirmación frente a la evidencia que tiene. Nunca dice que una afirmación esté probada: dice qué afirmaciones se apoyan en evidencia actual que pasa, cuáles en evidencia que falla, obsoleta o ausente, y cuáles solo en supuestos.

Escribir el caso

version: 1
goals:
  - id: G1
    statement: The assistant routes tickets well enough for first-line support
    scope: first-line support tickets in English
    strategy: argue over label accuracy and the misrouting hazard
    reassess_when: [the model changes, a new language is supported]
    goals:
      - id: G1.1
        statement: Labels are accurate
        evidence:
          - rule: label-floor
      - id: G1.2
        statement: Misrouting stays rare
        evidence:
          - hazard: missed-label
          - record: records/release-42.json
        defeaters:
          - id: D1
            statement: Tickets in other languages misroute
            resolved_by:
              - rule: label-floor
                suite: multilingual
      - id: G1.3
        statement: The deployment runs the model that was evaluated
        assumptions: [the model is pinned by digest in the deployment manifest]

Un objetivo es una afirmación. Un objetivo de nivel superior declara su scope, el uso previsto para el que se afirma; un subobjetivo lo hereda. strategy dice con palabras cómo los subobjetivos argumentan el objetivo. Cada elemento de evidence nombra exactamente uno de estos:

• rule: una regla de release.yaml, leída en la última ejecución de cada sistema en cada suite; system y suite acotan qué ejecuciones cuentan;
• hazard: un peligro de hazards.yaml (Registro de peligros);
• proof: una propiedad formal, leída como la lee una regla de prueba (Pruebas formales): el último resultado recibido para la propiedad, con prioridad para un DISPROVED del mismo modelo; model (un digest) la acota a un modelo formalizado; mientras el proyecto no tenga un resultado, el enlace no respalda nada;
• record: un archivo de registro de decisión escrito por oloproof record export, relativo a la raíz del proyecto.

assumptions es lo que el objetivo da por sentado. Un defeater es una razón por la que el objetivo podría ser falso; sigue abierto hasta que cada elemento de su evidencia resolved_by lo respalde. reassess_when dice qué debería hacer volver al equipo al objetivo.

Comprobarlo

oloproof assurance check

La comprobación rechaza un caso que nombra una regla que la política no tiene o un peligro que el registro no tiene, o cuyo objetivo de nivel superior no declara alcance, y termina con 2. Si no, imprime el árbol, cada objetivo con uno de cuatro estados:

• supported: cada elemento de su evidencia y cada subobjetivo lo respaldan, con evidencia actual, y no hay ningún refutador abierto;
• undermined: alguna evidencia falla, está obsoleta o está contradicha, un subobjetivo está socavado o hay un refutador abierto;
• assumptions_only: nada lo respalda y se apoya en supuestos declarados;
• unsupported: cualquier otro caso, con cada laguna nombrada. Un objetivo con algo de respaldo y una laguna no está respaldado: una afirmación es tan fuerte como lo más débil en que se apoya.

Una regla respalda un objetivo cuando cada última ejecución que la decidió dice PASS, y lo socava cuando alguna dice FAIL; INSUFFICIENT_EVIDENCE y MANUAL_REVIEW no respaldan nada. Un peligro respalda cuando pasa cada regla que lo mide. Un resultado formal respalda cuando la propiedad fue PROVED, y socava cuando fue DISPROVED o cuando dos resultados para un mismo modelo discrepan; un resultado dice lo que prueba sobre el modelo formalizado, nunca sobre el despliegue. Un registro respalda cuando el digest de su contenido sigue coincidiendo con su id y su decisión es PASS. La evidencia de una ejecución que ya no coincide con el proyecto (cambiaron su sistema, su suite, sus evaluadores o su política) está obsoleta y socava. Estos estados son del caso, nunca decisiones, y nunca cambian un código de salida. --json escribe el mismo informe para un pipeline.

Dónde aparece

oloproof run registra el caso con la ejecución, oloproof push lleva el caso de la ejecución a su espacio de trabajo con los resultados formales que nombran sus enlaces de prueba, y oloproof export escribe la lectura que hace el motor junto a los bundles. La página Safety and risk muestra el árbol con cada estado tal como lo escribió el motor, cada regla enlazada a su evidencia. En el espacio de trabajo, el caso se lee frente a las ejecuciones que usted envió con push: allí no se compara la vigencia, porque no hay archivo de proyecto con el que comparar, y los enlaces a registros solo los lee oloproof assurance check. Un registro de decisión nombra el caso que registró su ejecución; record verify lo presenta como la palabra del equipo.

Siguientes pasos

• Registro de peligros cubre los peligros en que puede apoyarse un objetivo.
• Grafo de evidencia dibuja cada afirmación con la evidencia que tiene debajo.