Przejdź do treści
Dokumentacja
Dziennik zmianCennikOtwórz konsolę

Przewodniki

Graf dowodów

Graf dowodów to wszystko, na czym opiera się decyzja o wydaniu, zapisane jako typowane węzły i typowane krawędzie w jednym pliku JSON. Zawiera wersje systemu, zestawu i ewaluatorów, które ocenił przebieg, oszacowania z niego obliczone, decyzje, które odczytały je według polityki, zatwierdzenia, które je zaakceptowały, zagrożenia, które mierzą, twierdzenia uzasadnienia zapewnienia, które wspierają, oraz wyniki formalne obok nich. Wskazuje też, gdzie dowody są niekompletne, nieaktualne lub sprzeczne, aby recenzent zobaczył luki, zanim przeczyta cokolwiek innego.

Rysowanie grafu

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

Bez przebiegu graf obejmuje ostatni przebieg każdego systemu na każdym zestawie, czyli te same przebiegi, względem których czytane są rejestr zagrożeń i uzasadnienie zapewnienia. Z identyfikatorem przebiegu obejmuje ten przebieg i każde twierdzenie, które go czyta. Z --record jest rysowany wyłącznie z pliku rekordu decyzji, więc druga strona może zobaczyć, co rekord zawiera, bez twojego magazynu; to, co rekord jedynie wymienia (jego rejestr zagrożeń i uzasadnienie zapewnienia, przez skrót), jest wypisane w uwagach. Bez --out graf jest wypisywany na ekran.

Co zawiera

Plik mówi "graph": "oloproof.evidence_graph/v1". Każdy węzeł ma id (typowane, na przykład run:run_01J9 lub decision:run_01J9/label-floor), type, label, attributes (stan, przedział, skrót) oraz basis, czyli to, na czym się opiera:

  • computed przez silnik z zapisanych dowodów: oszacowanie z przedziałem, decyzja;
  • signed przez zarejestrowany runner, którego podpis sprawdza oloproof record verify;
  • attested przez wskazane osoby: polityka wydań, zatwierdzenie, zagrożenie, twierdzenie;
  • imported z innego narzędzia: wyniki odczytane przez oloproof scores import, wynik solvera.

Typy węzłów to system_version, suite_version, evaluator_version, run, estimate, decision, policy, signoff, hazard, claim i proof. Krawędzie też są typowane: przebieg evaluates wersję systemu i działa on_suite na wersji zestawu; oszacowanie jest computed_from z przebiegu i judged_by przez wersję ewaluatora; decyzja reads oszacowanie under_policy według polityki; zatwierdzenie approves decyzję; zagrożenie jest measured_by przez decyzję; a twierdzenie jest supported_by przez decyzje, zagrożenia, wyniki formalne i swoje podcele.

Co zgłasza

  • dangling: krawędź, której celu graf nie zawiera, z podaniem przyczyny. Zagrożenie, które wymienia regułę nierozstrzygniętą przez żaden przebieg, albo decyzja, której metryka nie ma zapisanego wyniku, pojawia się tutaj, zamiast zniknąć.
  • stale: przebieg, którego dowody nie pasują już do tego, z czym jest porównywany, z każdą przyczyną i każdym węzłem, który się na nim opiera. Lokalnie przebieg jest porównywany z projektem w jego obecnym stanie; w przestrzeni roboczej, a także bez pliku projektu, z najnowszym przebiegiem tego samego systemu i zestawu w magazynie. Graf narysowany z rekordu nie zgłasza niczego nieaktualnego, bo nie ma go z czym porównać.
  • contradictions: dwa wyniki formalne dla jednej własności i jednego modelu, które się nie zgadzają, oraz twierdzenie uzasadniane dowodami z wynikiem negatywnym.

Nic w grafie niczego nie rozstrzyga: stany to decyzje silnika, a status twierdzenia to ten, który zgłasza oloproof assurance check.

W przestrzeni roboczej

Strona dowodów przebiegu udostępnia graf do pobrania, narysowany przez silnik z dowodów, które wypchnąłeś, obok rekordu decyzji zarządzanego przebiegu.

Co dalej