Ga naar de inhoud
Docs
WijzigingslogboekPrijzenConsole openen

Handleidingen

Assurance cases

Een assurance case is het argument van uw team dat een systeem goed genoeg is voor een opgegeven gebruik: elke bewering, waarvoor ze geldt en het bewijs waarop ze rust. De case staat naast het releasebeleid in assurance.yaml, wordt dus in pull requests beoordeeld, en Oloproof leest elke bewering tegen het bewijs dat het bewaart. Het zegt nooit dat een bewering bewezen is: het zegt welke beweringen rusten op actueel bewijs dat slaagt, welke op bewijs dat faalt, verouderd is of ontbreekt, en welke alleen op aannames.

De case schrijven

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]

Een doel is een bewering. Een doel op het hoogste niveau noemt zijn scope, het beoogde gebruik waarvoor het wordt beweerd; een subdoel erft die. strategy zegt in woorden hoe de subdoelen het doel onderbouwen. Elk stuk evidence noemt precies één van:

  • rule: een regel uit release.yaml, gelezen bij de laatste run van elk systeem op elke suite; system en suite beperken welke runs tellen;
  • hazard: een gevaar uit hazards.yaml (Gevarenregister);
  • proof: een formele eigenschap, gelezen zoals een bewijsregel haar leest (Formele bewijzen): het laatst ontvangen resultaat voor de eigenschap, waarbij een DISPROVED van hetzelfde model wint; model (een digest) beperkt haar tot één geformaliseerd model; zolang het project geen resultaat heeft, ondersteunt de koppeling niets;
  • record: een beslissingsrecordbestand geschreven door oloproof record export, relatief ten opzichte van de projectroot.

assumptions zijn wat het doel als gegeven aanneemt. Een defeater is een reden waarom het doel onwaar zou kunnen zijn; die blijft open tot elk stuk bewijs in zijn resolved_by het ondersteunt. reassess_when zegt wat het team terug naar het doel moet sturen.

Het controleren

oloproof assurance check

De controle weigert een case die een regel noemt die het beleid niet bevat of een gevaar dat het register niet bevat, of waarvan het hoogste doel geen scope noemt, en eindigt met 2. Anders drukt ze de boom af, elk doel met een van vier statussen:

  • supported: elk stuk van zijn bewijs en elk subdoel ondersteunt het, op actueel bewijs, en geen defeater staat open;
  • undermined: enig bewijs faalt, is verouderd of wordt tegengesproken, een subdoel is ondermijnd, of een defeater staat open;
  • assumptions_only: niets ondersteunt het, en het rust op vermelde aannames;
  • unsupported: al het andere, met elk gat bij naam genoemd. Een doel met enige ondersteuning en een gat is niet ondersteund: een bewering is zo sterk als het zwakste waarop ze rust.

Een regel ondersteunt een doel wanneer elke laatste run die haar besliste PASS zegt, en ondermijnt het wanneer er een FAIL zegt; INSUFFICIENT_EVIDENCE en MANUAL_REVIEW ondersteunen niets. Een gevaar ondersteunt wanneer elke regel die het meet slaagt. Een formeel resultaat ondersteunt wanneer de eigenschap PROVED was, en ondermijnt wanneer ze DISPROVED was of wanneer twee resultaten voor één model elkaar tegenspreken; een resultaat zegt wat het bewijst over het geformaliseerde model, nooit over de uitrol. Een record ondersteunt wanneer de digest van zijn inhoud nog steeds zijn id is en zijn beslissing PASS is. Bewijs uit een run die niet meer bij het project past (zijn systeem, suite, evaluators of beleid veranderden) is verouderd en ondermijnt. Deze statussen zijn van de case, nooit beslissingen, en ze veranderen nooit een exitcode. --json schrijft hetzelfde rapport voor een pipeline.

Waar het verschijnt

oloproof run legt de case vast bij de run, oloproof push brengt de case van de run naar uw werkruimte met de formele resultaten die zijn bewijskoppelingen noemen, en oloproof export schrijft de lezing ervan door de engine naast de bundels. De pagina Safety and risk toont de boom met elke status zoals de engine hem schreef, elke regel gekoppeld aan zijn bewijs. In de werkruimte wordt de case gelezen tegen de runs die u pushte: actualiteit wordt daar niet vergeleken, omdat er geen projectbestand is om mee te vergelijken, en recordkoppelingen worden alleen gelezen door oloproof assurance check. Een beslissingsrecord noemt de case die zijn run vastlegde; record verify vermeldt die als het woord van het team.

Verder lezen