Grafo delle evidenze

Il grafo delle evidenze è tutto ciò su cui poggia una decisione di rilascio, scritto come nodi tipizzati e archi tipizzati in un unico file JSON. Contiene le versioni di sistema, suite e valutatore che un'esecuzione ha valutato, le stime calcolate da essa, le decisioni che le leggono secondo una policy, le approvazioni che le hanno convalidate, i pericoli che misurano, le affermazioni del caso di garanzia che sostengono e i risultati formali accanto. Indica anche dove l'evidenza è incompleta, non aggiornata o in conflitto, così che un revisore veda le lacune prima di leggere qualsiasi altra cosa.

Disegnarlo

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

Senza un'esecuzione, il grafo copre l'ultima esecuzione di ogni sistema su ogni suite, le stesse esecuzioni rispetto a cui si leggono il registro dei pericoli e il caso di garanzia. Con un id di esecuzione, copre quell'esecuzione e ogni affermazione che la legge. Con --record, è disegnato a partire dal solo file di un record di decisione, così che una seconda parte possa vedere che cosa porta il record senza il vostro archivio; ciò che il record si limita a nominare (il suo registro dei pericoli e il suo caso di garanzia, per digest) è elencato nelle note. Senza --out il grafo viene stampato.

Che cosa contiene

Il file dice "graph": "oloproof.evidence_graph/v1". Ogni nodo ha un id (tipizzato, come run:run_01J9 o decision:run_01J9/label-floor), un type, un label, degli attributes (uno stato, un intervallo, un digest) e una basis, ciò su cui poggia:

• computed dal motore a partire da evidenza registrata: una stima con il suo intervallo, una decisione;
• signed da un runner registrato, la cui firma è verificata da oloproof record verify;
• attested da persone nominate: la policy di rilascio, un'approvazione, un pericolo, un'affermazione;
• imported da un altro strumento: punteggi letti da oloproof scores import, il risultato di un solver.

I tipi di nodo sono system_version, suite_version, evaluator_version, run, estimate, decision, policy, signoff, hazard, claim e proof. Anche gli archi sono tipizzati: un'esecuzione evaluates una versione di sistema e gira on_suite su una versione di suite; una stima è computed_from un'esecuzione e judged_by una versione di valutatore; una decisione reads una stima under_policy una policy; un'approvazione approves una decisione; un pericolo è measured_by una decisione; e un'affermazione è supported_by decisioni, pericoli, risultati formali e i suoi sotto-obiettivi.

Che cosa riporta

• dangling: un arco la cui destinazione non è nel grafo, con il motivo. Un pericolo che nomina una regola che un'esecuzione non ha deciso, o una decisione la cui metrica non ha alcun risultato memorizzato, compare qui invece di sparire.
• stale: un'esecuzione la cui evidenza non corrisponde più a ciò con cui è confrontata, con ogni motivo e ogni nodo che poggia su di essa. In locale un'esecuzione è confrontata con il progetto com'è ora; nello spazio di lavoro, e senza file di progetto, con l'esecuzione più recente nell'archivio per lo stesso sistema e la stessa suite. Un grafo disegnato da un record non riporta nulla di non aggiornato, poiché non c'è nulla con cui confrontarlo.
• contradictions: due risultati formali per una stessa proprietà e uno stesso modello che discordano, e un'affermazione argomentata da evidenza che fallisce.

Nulla nel grafo decide alcunché: gli stati sono le decisioni del motore, e lo stato di un'affermazione è quello che riporta oloproof assurance check.

Nello spazio di lavoro

La pagina delle evidenze di un'esecuzione offre il grafo da scaricare, disegnato dal motore a partire dall'evidenza che avete inviato, accanto al record di decisione di un'esecuzione governata.

Dove andare dopo

• Casi di garanzia tratta le affermazioni che il grafo disegna.
• Registro dei pericoli tratta i pericoli che una decisione misura.