Assurance Cases

Ein Assurance Case ist die Argumentation Ihres Teams, dass ein System für einen genannten Einsatz gut genug ist. Er nennt jede Behauptung, den Einsatz, für den sie aufgestellt wird, und die Evidenz, auf der sie ruht. Der Case liegt neben der Release-Policy in assurance.yaml, wird also in Pull Requests geprüft, und Oloproof liest jede Behauptung gegen die Evidenz, die es hält. Oloproof erklärt eine Behauptung nie für bewiesen: Es sagt, welche Behauptungen auf aktueller bestandener Evidenz ruhen, welche auf fehlschlagender, veralteter oder fehlender Evidenz und welche allein auf Annahmen.

Den Case schreiben

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]

Ein Ziel ist eine Behauptung. Ein Ziel der obersten Ebene nennt seinen scope, den vorgesehenen Einsatz, für den es behauptet wird; ein Unterziel erbt ihn. strategy sagt in Worten, wie die Unterziele das Ziel begründen. Jedes Stück evidence nennt genau eines davon:

• rule: eine Regel aus release.yaml, gelesen beim letzten Lauf jedes Systems auf jeder Suite; system und suite grenzen ein, welche Läufe zählen;
• hazard: eine Gefährdung aus hazards.yaml (Gefährdungsregister);
• proof: eine formale Eigenschaft, gelesen so, wie eine Beweisregel sie liest (Formale Beweise): das zuletzt empfangene Ergebnis für die Eigenschaft, wobei ein DISPROVED desselben Modells gewinnt; model (ein Digest) schränkt es auf ein formalisiertes Modell ein; solange das Projekt kein Ergebnis hält, stützt der Verweis nichts;
• record: eine Datei mit einem Entscheidungsdatensatz, geschrieben von oloproof record export, relativ zum Wurzelverzeichnis des Projekts.

assumptions sind das, was das Ziel als gegeben voraussetzt. Ein defeater ist ein Grund, warum das Ziel falsch sein könnte; er bleibt offen, bis jedes Stück seiner Evidenz unter resolved_by ihn stützt. reassess_when sagt, was das Team zu dem Ziel zurückschicken sollte.

Es prüfen

oloproof assurance check

Die Prüfung lehnt einen Case ab, der eine Regel nennt, die die Policy nicht enthält, oder eine Gefährdung, die das Register nicht enthält, oder dessen Ziel der obersten Ebene keinen Einsatzbereich nennt, und endet mit 2. Sonst gibt sie den Baum aus, jedes Ziel mit einem von vier Status:

• supported: jedes Stück seiner Evidenz und jedes Unterziel stützt es, auf aktueller Evidenz, und kein Einwand ist offen;
• undermined: eine Evidenz schlägt fehl, ist veraltet oder wird widerlegt, ein Unterziel ist untergraben, oder ein Einwand ist offen;
• assumptions_only: nichts stützt es, und es ruht auf genannten Annahmen;
• unsupported: alles andere, mit jeder Lücke benannt. Ein Ziel mit etwas Stützung und einer Lücke ist ungestützt: Eine Behauptung ist so stark wie das Schwächste, worauf sie ruht.

Eine Regel stützt ein Ziel, wenn jeder letzte Lauf, der sie entschieden hat, PASS sagt, und untergräbt es, wenn einer FAIL sagt; INSUFFICIENT_EVIDENCE und MANUAL_REVIEW stützen nichts. Eine Gefährdung stützt, wenn jede Regel, die sie misst, besteht. Ein formales Ergebnis stützt, wenn die Eigenschaft PROVED wurde, und untergräbt, wenn sie DISPROVED wurde oder wenn zwei Ergebnisse für ein Modell einander widersprechen; ein Ergebnis sagt, was es über das formalisierte Modell beweist, nie über die Bereitstellung. Ein Datensatz stützt, wenn sein Inhalt noch auf seine ID hasht und seine Entscheidung PASS ist. Evidenz aus einem Lauf, der nicht mehr zum Projekt passt (sein System, seine Suite, seine Evaluatoren oder seine Policy haben sich geändert), ist veraltet und untergräbt. Diese Status gehören dem Case, sind nie Entscheidungen und ändern nie einen Exit-Code. --json schreibt denselben Bericht für eine Pipeline.

Wo es erscheint

oloproof run hält den Case mit dem Lauf fest, oloproof push bringt den Case des Laufs mit den formalen Ergebnissen, die seine Beweisverweise nennen, in Ihren Workspace, und oloproof export schreibt die Lesart der Engine neben die Bundles. Die Seite Safety and risk zeigt den Baum mit jedem Status so, wie die Engine ihn geschrieben hat, jede Regel mit ihrer Evidenz verlinkt. Im Workspace wird der Case gegen die Läufe gelesen, die Sie gepusht haben: Die Aktualität wird dort nicht verglichen, weil es keine Projektdatei gibt, mit der man vergleichen könnte, und Verweise auf Datensätze liest nur oloproof assurance check. Ein Entscheidungsdatensatz nennt den Case, den sein Lauf festgehalten hat; record verify führt ihn als Wort des Teams.

Wie es weitergeht

• Gefährdungsregister behandelt die Gefährdungen, auf denen ein Ziel ruhen kann.
• Evidenzgraph zeichnet jede Behauptung mit der Evidenz darunter.