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

Hồ sơ đảm bảo

Hồ sơ đảm bảo là lập luận của nhóm bạn rằng một hệ thống đủ tốt cho một mục đích sử dụng đã nêu: từng khẳng định, mục đích nó hướng tới, và bằng chứng nó dựa vào. Hồ sơ nằm cạnh chính sách phát hành trong assurance.yaml, nên được xem xét trong pull request, và Oloproof đọc từng khẳng định theo bằng chứng mà nó nắm giữ. Nó không bao giờ nói một khẳng định đã được chứng minh: nó nói khẳng định nào dựa trên bằng chứng đạt và còn hiện hành, khẳng định nào dựa trên bằng chứng thất bại, lỗi thời hoặc còn thiếu, và khẳng định nào chỉ dựa trên giả định.

Viết hồ sơ

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]

Một mục tiêu là một khẳng định. Mục tiêu cấp cao nhất nêu scope của nó, tức mục đích sử dụng dự kiến mà khẳng định hướng tới; mục tiêu con kế thừa phạm vi đó. strategy nói bằng lời cách các mục tiêu con lập luận cho mục tiêu. Mỗi mục evidence nêu đúng một trong các loại sau:

  • rule: một quy tắc của release.yaml, được đọc ở lần chạy mới nhất của mỗi hệ thống trên mỗi bộ kiểm thử; system và suite thu hẹp những lần chạy được tính;
  • hazard: một mối nguy của hazards.yaml (Sổ đăng ký mối nguy);
  • proof: một thuộc tính hình thức, được đọc như một quy tắc chứng minh đọc nó (Chứng minh hình thức): kết quả cuối cùng nhận được cho thuộc tính, trong đó một DISPROVED của cùng mô hình thắng; model (một digest) thu hẹp nó về một mô hình đã hình thức hóa; chừng nào dự án chưa có kết quả, liên kết này không hỗ trợ gì cả;
  • record: một tệp bản ghi quyết định do oloproof record export ghi, với đường dẫn tương đối so với thư mục gốc của dự án.

assumptions là những gì mục tiêu coi là đương nhiên. Một defeater là một lý do khiến mục tiêu có thể sai; nó vẫn mở cho đến khi mọi mục bằng chứng trong resolved_by của nó đều hỗ trợ nó. reassess_when nói điều gì sẽ khiến nhóm quay lại xem xét mục tiêu.

Kiểm tra

oloproof assurance check

Lệnh kiểm tra từ chối một hồ sơ nêu một quy tắc không có trong chính sách hoặc một mối nguy không có trong sổ đăng ký, hoặc có mục tiêu cấp cao nhất không nêu phạm vi, và thoát với 2. Nếu không, nó in ra cây mục tiêu, mỗi mục tiêu với một trong bốn trạng thái:

  • supported: mọi mục bằng chứng và mọi mục tiêu con của nó đều hỗ trợ nó, trên bằng chứng hiện hành, và không có phản bác nào đang mở;
  • undermined: một phần bằng chứng thất bại, lỗi thời hoặc bị mâu thuẫn, một mục tiêu con bị suy yếu, hoặc một phản bác đang mở;
  • assumptions_only: không có gì hỗ trợ nó, và nó dựa trên các giả định đã nêu;
  • unsupported: mọi trường hợp còn lại, với từng khoảng trống được nêu tên. Một mục tiêu có một phần hỗ trợ và một khoảng trống là không được hỗ trợ: một khẳng định chỉ mạnh bằng điều yếu nhất mà nó dựa vào.

Một quy tắc hỗ trợ một mục tiêu khi mọi lần chạy mới nhất đã quyết định quy tắc đó đều nói PASS, và làm suy yếu mục tiêu khi có bất kỳ lần nào nói FAIL; INSUFFICIENT_EVIDENCE và MANUAL_REVIEW không hỗ trợ gì cả. Một mối nguy hỗ trợ khi mọi quy tắc đo nó đều đạt. Một kết quả hình thức hỗ trợ khi thuộc tính ở trạng thái PROVED, và làm suy yếu khi nó ở trạng thái DISPROVED hoặc khi hai kết quả cho cùng một mô hình mâu thuẫn nhau; một kết quả nói điều nó chứng minh về mô hình đã được hình thức hóa, không bao giờ về bản triển khai. Một bản ghi hỗ trợ khi nội dung của nó vẫn cho ra digest trùng với id của nó và quyết định của nó là PASS. Bằng chứng từ một lần chạy không còn khớp với dự án (hệ thống, bộ kiểm thử, bộ đánh giá hoặc chính sách của nó đã thay đổi) là lỗi thời và làm suy yếu mục tiêu. Các trạng thái này là của hồ sơ, không bao giờ là quyết định, và chúng không bao giờ thay đổi mã thoát. --json ghi cùng báo cáo đó cho một pipeline.

Nơi nó xuất hiện

oloproof run ghi hồ sơ cùng lần chạy, oloproof push đưa hồ sơ của lần chạy tới không gian làm việc của bạn cùng các kết quả hình thức mà các liên kết chứng minh của nó nêu tên, và oloproof export ghi cách công cụ đọc nó cạnh các gói. Trang Safety and risk hiển thị cây mục tiêu với mỗi trạng thái đúng như công cụ đã ghi, mỗi quy tắc liên kết tới bằng chứng của nó. Trong không gian làm việc, hồ sơ được đọc theo các lần chạy bạn đã đẩy lên: độ mới không được so sánh ở đó, vì không có tệp dự án nào để so sánh, và các liên kết tới bản ghi chỉ được đọc bởi oloproof assurance check. Một bản ghi quyết định nêu hồ sơ mà lần chạy của nó đã ghi; record verify báo nó là lời của nhóm.

Tiếp theo