Chuyển đến nội dung
Tài liệu
Nhật ký thay đổiGiáMở bảng điều khiển

Hướng dẫn

Đồ thị bằng chứng

Đồ thị bằng chứng là mọi thứ mà một quyết định phát hành dựa vào, được viết thành các nút có kiểu và các cạnh có kiểu trong một tệp JSON. Nó chứa các phiên bản hệ thống, bộ kiểm thử và bộ đánh giá mà một lần chạy đã đánh giá, các ước lượng được tính từ lần chạy đó, các quyết định đọc những ước lượng ấy theo một chính sách, các lượt phê duyệt đã chấp thuận những quyết định đó, các mối nguy mà chúng đo, các khẳng định của hồ sơ đảm bảo mà chúng hỗ trợ và các kết quả hình thức bên cạnh. Nó cũng nêu những chỗ bằng chứng chưa đầy đủ, đã lỗi thời hoặc mâu thuẫn, để người xem xét thấy các khoảng trống trước khi đọc bất cứ điều gì khác.

Vẽ đồ thị

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

Khi không chỉ định lần chạy, đồ thị bao gồm lần chạy mới nhất của mỗi hệ thống trên mỗi bộ kiểm thử, cũng chính là các lần chạy mà sổ đăng ký mối nguy và hồ sơ đảm bảo được đọc theo. Với một id lần chạy, nó bao gồm lần chạy đó và mọi khẳng định đọc lần chạy đó. Với --record, nó được vẽ chỉ từ một tệp bản ghi quyết định, để một bên thứ hai có thể thấy bản ghi mang những gì mà không cần kho lưu trữ của bạn; những gì bản ghi chỉ nêu tên (sổ đăng ký mối nguy và hồ sơ đảm bảo của nó, theo digest) được liệt kê trong phần ghi chú. Khi không có --out, đồ thị được in ra.

Bên trong có gì

Tệp ghi "graph": "oloproof.evidence_graph/v1". Mỗi nút có một id (có kiểu, chẳng hạn run:run_01J9 hoặc decision:run_01J9/label-floor), một type, một label, attributes (một trạng thái, một khoảng, một digest) và một basis, tức điều mà nó dựa vào:

  • computed bởi công cụ từ bằng chứng đã ghi: một ước lượng cùng khoảng của nó, một quyết định;
  • signed bởi một runner đã đăng ký, có chữ ký được oloproof record verify kiểm tra;
  • attested bởi những người có tên: chính sách phát hành, một lượt phê duyệt, một mối nguy, một khẳng định;
  • imported từ một công cụ khác: các điểm được đọc bởi oloproof scores import, kết quả của một bộ giải.

Các kiểu nút là system_version, suite_version, evaluator_version, run, estimate, decision, policy, signoff, hazard, claim và proof. Các cạnh cũng có kiểu: một lần chạy evaluates một phiên bản hệ thống và chạy on_suite một phiên bản bộ kiểm thử; một ước lượng được computed_from một lần chạy và judged_by một phiên bản bộ đánh giá; một quyết định reads một ước lượng under_policy một chính sách; một lượt phê duyệt approves một quyết định; một mối nguy được measured_by một quyết định; và một khẳng định được supported_by các quyết định, mối nguy, kết quả hình thức và các mục tiêu con của nó.

Nó báo cáo gì

  • dangling: một cạnh có đích mà đồ thị không chứa, kèm lý do. Một mối nguy nêu một quy tắc mà lần chạy không quyết định, hoặc một quyết định có chỉ số không có kết quả đã lưu, sẽ xuất hiện ở đây thay vì biến mất.
  • stale: một lần chạy có bằng chứng không còn khớp với thứ mà nó được so sánh, kèm từng lý do và mọi nút dựa vào nó. Ở máy cục bộ, một lần chạy được so sánh với dự án như hiện tại; trong không gian làm việc, và khi không có tệp dự án, thì với lần chạy mới nhất trong kho của cùng hệ thống và bộ kiểm thử. Một đồ thị vẽ từ một bản ghi không báo cáo gì lỗi thời, vì không có gì để so sánh với nó.
  • contradictions: hai kết quả hình thức cho cùng một thuộc tính và cùng một mô hình mà mâu thuẫn nhau, và một khẳng định được lập luận từ bằng chứng thất bại.

Không có gì trong đồ thị quyết định điều gì: các trạng thái là quyết định của công cụ, và trạng thái của một khẳng định là trạng thái mà oloproof assurance check báo cáo.

Trong không gian làm việc

Trang bằng chứng của một lần chạy cho phép tải đồ thị xuống, do công cụ vẽ từ bằng chứng bạn đã đẩy lên, bên cạnh bản ghi quyết định của một lần chạy được quản trị.

Tiếp theo