Bewijsgraaf

De bewijsgraaf is alles waarop een releasebeslissing rust, geschreven als getypeerde knopen en getypeerde randen in één JSON-bestand. Hij bevat de versies van systeem, suite en evaluator die een run evalueerde, de schattingen die eruit werden berekend, de beslissingen die ze onder een beleid lazen, de sign-offs die die beslissingen goedkeurden, de gevaren die ze meten, de beweringen van de assurance case die ze ondersteunen en de formele resultaten ernaast. Hij noemt ook waar het bewijs onvolledig, verouderd of tegenstrijdig is, zodat een beoordelaar de gaten ziet voordat hij iets anders leest.

Hem tekenen

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

Zonder run omvat de graaf de laatste run van elk systeem op elke suite, dezelfde runs waartegen het gevarenregister en de assurance case worden gelezen. Met een run-id omvat hij die run en elke bewering die hem leest. Met --record wordt hij alleen uit een beslissingsrecordbestand getekend, zodat een tweede partij zonder uw opslag kan zien wat het record meedraagt; wat het record alleen noemt (zijn gevarenregister en zijn assurance case, via digest) staat in de notities. Zonder --out wordt de graaf afgedrukt.

Wat erin staat

Het bestand zegt "graph": "oloproof.evidence_graph/v1". Elke knoop heeft een id (getypeerd, zoals run:run_01J9 of decision:run_01J9/label-floor), een type, een label, attributes (een toestand, een interval, een digest) en een basis, waarop hij rust:

• computed door de engine uit vastgelegd bewijs: een schatting met haar interval, een beslissing;
• signed door een geregistreerde runner, wiens handtekening oloproof record verify controleert;
• attested door mensen bij naam: het releasebeleid, een sign-off, een gevaar, een bewering;
• imported uit een ander hulpmiddel: scores gelezen door oloproof scores import, het resultaat van een solver.

De knooptypen zijn system_version, suite_version, evaluator_version, run, estimate, decision, policy, signoff, hazard, claim en proof. Ook de randen zijn getypeerd: een run evaluates een systeemversie en draait on_suite een suiteversie; een schatting is computed_from een run en judged_by een evaluatorversie; een beslissing reads een schatting under_policy een beleid; een sign-off approves een beslissing; een gevaar is measured_by een beslissing; en een bewering is supported_by beslissingen, gevaren, formele resultaten en haar subdoelen.

Wat hij meldt

• dangling: een rand waarvan de graaf het doel niet bevat, met de reden. Een gevaar dat een regel noemt die geen run besliste, of een beslissing waarvan de metriek geen opgeslagen resultaat heeft, verschijnt hier in plaats van te verdwijnen.
• stale: een run waarvan het bewijs niet meer overeenkomt met waarmee het wordt vergeleken, met elke reden en elke knoop die erop rust. Lokaal wordt een run vergeleken met het project zoals het nu is; in de werkruimte, en zonder projectbestand, met de nieuwste run van hetzelfde systeem en dezelfde suite in de opslag. Een graaf die uit een record is getekend, meldt niets als verouderd, omdat er niets is om mee te vergelijken.
• contradictions: twee formele resultaten voor één eigenschap en één model die elkaar tegenspreken, en een bewering die wordt onderbouwd met bewijs dat faalt.

Niets in de graaf beslist iets: de toestanden zijn de beslissingen van de engine, en de status van een bewering is die welke oloproof assurance check meldt.

In de werkruimte

De bewijspagina van een run biedt de graaf aan als download, door de engine getekend uit het bewijs dat u pushte, naast het beslissingsrecord van een run onder governance.

Verder lezen

• Assurance cases behandelt de beweringen die de graaf tekent.
• Gevarenregister behandelt de gevaren die een beslissing meet.