Grafo de evidencia

El grafo de evidencia es todo aquello en que se apoya una decisión de publicación, escrito como nodos tipados y aristas tipadas en un solo archivo JSON. Contiene las versiones de sistema, suite y evaluador que evaluó una ejecución, las estimaciones calculadas a partir de ella, las decisiones que las leen bajo una política, las aprobaciones que las aprobaron, los peligros que miden, las afirmaciones del caso de aseguramiento que respaldan y los resultados formales que hay junto a ellas. También nombra dónde la evidencia está incompleta, obsoleta o en conflicto, para que quien revisa vea las lagunas antes de leer nada más.

Dibujarlo

oloproof evidence graph --out graph.json
oloproof evidence graph run_01J9 --out run.json
oloproof evidence graph --record decision-record.json --out record-graph.json

Sin una ejecución, el grafo cubre la última ejecución de cada sistema en cada suite, las mismas ejecuciones frente a las que se leen el registro de peligros y el caso de aseguramiento. Con un id de ejecución, cubre esa ejecución y cada afirmación que la lee. Con --record, se dibuja solo a partir de un archivo de registro de decisión, para que otra parte vea lo que contiene el registro sin su almacén; lo que el registro solo nombra (su registro de peligros y su caso de aseguramiento, por digest) aparece en las notas. Sin --out, el grafo se imprime.

Qué contiene

El archivo dice "graph": "oloproof.evidence_graph/v1". Cada nodo tiene un id (tipado, como run:run_01J9 o decision:run_01J9/label-floor), un type, un label, attributes (un estado, un intervalo, un digest) y una basis, aquello en que se apoya:

• computed por el motor a partir de evidencia registrada: una estimación con su intervalo, una decisión;
• signed por un runner registrado, cuya firma comprueba oloproof record verify;
• attested por personas con nombre: la política de publicación, una aprobación, un peligro, una afirmación;
• imported de otra herramienta: puntuaciones leídas por oloproof scores import, el resultado de un solver.

Los tipos de nodo son system_version, suite_version, evaluator_version, run, estimate, decision, policy, signoff, hazard, claim y proof. Las aristas también son tipadas: una ejecución evaluates una versión de sistema y se ejecuta on_suite una versión de suite; una estimación es computed_from una ejecución y judged_by una versión de evaluador; una decisión reads una estimación under_policy una política; una aprobación approves una decisión; un peligro es measured_by una decisión; y una afirmación es supported_by decisiones, peligros, resultados formales y sus subobjetivos.

Qué informa

• dangling: una arista cuyo destino el grafo no contiene, con el motivo. Un peligro que nombra una regla que ninguna ejecución decidió, o una decisión cuya métrica no tiene resultado almacenado, aparece aquí en lugar de desaparecer.
• stale: una ejecución cuya evidencia ya no coincide con aquello con lo que se compara, con cada motivo y cada nodo que se apoya en ella. En local, una ejecución se compara con el proyecto tal como está ahora; en el espacio de trabajo, y sin archivo de proyecto, con la ejecución más reciente del mismo sistema y la misma suite en el almacén. Un grafo dibujado a partir de un registro no informa nada obsoleto, ya que no hay nada con lo que compararlo.
• contradictions: dos resultados formales para una misma propiedad y un mismo modelo que discrepan, y una afirmación argumentada a partir de evidencia que falla.

Nada en el grafo decide nada: los estados son las decisiones del motor, y el estado de una afirmación es el que informa oloproof assurance check.

En el espacio de trabajo

La página de evidencia de una ejecución ofrece el grafo para descargar, dibujado por el motor a partir de la evidencia que usted envió con push, junto al registro de decisión de una ejecución gobernada.

Siguientes pasos

• Casos de aseguramiento cubre las afirmaciones que dibuja el grafo.
• Registro de peligros cubre los peligros que mide una decisión.