Nội dung bài viết
Harmonic ngày 27/10 công bố mở rộng Aristotle từ chứng minh toán học sang kiểm chứng phần mềm và phần cứng, bắt đầu với C và Verilog. Thông tin được Reuters phản ánh trong bối cảnh AI ngày càng tham gia phát hiện và đánh giá lỗi. Đây là hướng bổ sung cho quy trình kỹ thuật, không phải lời bảo đảm mọi sản phẩm qua công cụ đều không còn rủi ro.
Điểm khác biệt của kiểm chứng hình thức là yêu cầu được diễn đạt theo cách có thể kiểm tra bằng lập luận chặt chẽ. Nó đặt câu hỏi một tính chất đã nêu có đúng trong mô hình và những điều kiện được xác định hay không.
Điều được chứng minh phải được viết ra trước
Một hệ thống có thể đáp ứng đúng yêu cầu đã mô tả nhưng bản thân yêu cầu vẫn thiếu. Nếu phần quan trọng của tình huống không nằm trong mô hình, kết quả chứng minh không tự bao phủ phần đó. Đây là giới hạn cần được giải thích khi giới thiệu công nghệ.
Vì vậy, công việc không chỉ là đưa mã vào rồi nhận nhãn an toàn. Nhóm kỹ thuật cần xác định thuộc tính muốn kiểm tra, giả định đang sử dụng và quan hệ với môi trường thực thi. Sự rõ ràng ở đầu vào ảnh hưởng trực tiếp giá trị của kết quả.
Kiểm thử và chứng minh trả lời các câu hỏi khác nhau
Kiểm thử quan sát chương trình trong những trường hợp được chạy. Kiểm chứng hình thức có thể xem xét một tính chất theo mô hình đã thiết lập. Hai cách tiếp cận có thể bổ sung cho nhau, thay vì bị giới thiệu như lựa chọn loại bỏ hoàn toàn phương pháp còn lại.
Trong một dự án, vẫn cần xem sản phẩm có hoạt động đúng mục đích và kết nối phù hợp với các phần khác hay không. Một tính chất được chứng minh riêng không thay thế toàn bộ đánh giá thiết kế, vận hành hoặc trải nghiệm thực tế.
Nếu một yêu cầu được sửa trong quá trình phát triển, phần kiểm chứng liên quan cũng cần được xem lại. Một kết quả đúng cho phiên bản trước không mặc nhiên giữ nguyên ý nghĩa ở phiên bản mới. Nhóm cần lưu được quan hệ giữa mã, yêu cầu và bằng chứng đã kiểm tra. Việc quản lý phiên bản vì vậy có vai trò thiết thực, kể cả khi công cụ AI giúp rút ngắn một số thao tác kỹ thuật.
AI giúp công việc tiếp cận được hơn nhưng cần người đánh giá
Tự động hóa có thể giảm công sức ở một số bước tạo hoặc kiểm tra lập luận. Tuy nhiên, người sử dụng cần hiểu công cụ nhận đầu vào gì và kết quả đang khẳng định điều nào. Nếu không, một thông báo thành công rất dễ bị hiểu rộng hơn phạm vi kỹ thuật.
Tài liệu, khả năng lưu lại quá trình và cách xử lý khi công cụ không hoàn tất đều ảnh hưởng việc sử dụng trong nhóm. Quy trình phải giúp người khác kiểm tra lại, thay vì chỉ dựa vào một lần trao đổi với hệ thống.
Ý nghĩa thực tế nằm ở chỗ đặt công cụ vào quy trình
Một hướng thử hợp lý là chọn thành phần và tính chất có giới hạn rõ, rồi đánh giá công sức cũng như giá trị nhận được. Nhóm phụ trách cần xem kết quả có giúp ra quyết định tốt hơn hay chỉ thêm một bước khó giải thích.
Việc Harmonic mở rộng Aristotle cho thấy nhu cầu dùng AI để hỗ trợ công việc kiểm chứng đang tăng. Tuy vậy, câu chuyện đáng theo dõi không phải lời hứa chứng minh được tất cả. Đó là khả năng làm rõ điều kiện, kiểm tra được lập luận và giúp kỹ sư hiểu chính xác phần nào trong sản phẩm đã được xem xét.
Xem thêm Khoa học máy tính trên Tinh Hoa Số.
