Phương pháp hình thức: Chỉ là thực hành kỹ thuật tốt thôi sao? (2024)

• Giới thiệu

  • Marc Brooker là một kỹ sư tại AWS, phụ trách cơ sở dữ liệu và hệ thống serverless, đồng thời nhấn mạnh tầm quan trọng của formal methods trong kỹ nghệ phần mềm.

• Tầm quan trọng của formal methods

  • Formal methods là yếu tố thiết yếu để tiết kiệm thời gian và chi phí trong các hệ thống quy mô lớn, hệ thống phân tán và các hệ thống mức thấp quan trọng.
  • Kỹ nghệ phần mềm là bài toán tối ưu hóa thời gian và chi phí.
  • Formal methods giúp giảm chi phí làm lại và xử lý các thay đổi giao diện từ sớm, qua đó nâng cao tốc độ và hiệu quả phát triển phần mềm.

• Phạm vi áp dụng của formal methods

  • Với phần mềm được dẫn dắt bởi các yêu cầu người dùng thay đổi nhanh chóng, giá trị của formal methods có thể bị giới hạn.
  • Trong các hệ thống quy mô lớn, phân tán và mức thấp, formal methods giúp giảm đáng kể công việc làm lại và mật độ lỗi.

• Formal methods và công cụ

  • Formal methods và suy luận tự động bao gồm nhiều công cụ khác nhau, và được sử dụng hữu ích trong các hệ thống cloud quy mô lớn của AWS.
  • Có các ngôn ngữ đặc tả như TLA+, P, Alloy, cùng model checker, công cụ mô phỏng quyết định và ngôn ngữ lập trình có nhận thức về kiểm chứng.

• Kết luận

  • Những công cụ giúp suy nghĩ về thiết kế hệ thống ở giai đoạn thiết kế sẽ tăng tốc phát triển phần mềm, giảm rủi ro và cho phép xây dựng hệ thống tối ưu.
  • Với các kỹ sư xử lý hệ thống quy mô lớn và phức tạp, formal methods là một phần của thực hành kỹ thuật tốt.

[GN⁺]

Ý kiến Hacker News

• Việc xác minh hình thức của phần mềm phụ thuộc rất nhiều vào loại phần mềm và quy trình phát triển. Phần lớn các dự án phần mềm không tương thích với các yêu cầu hình thức

  • Việc phát triển và thiết kế phần mềm thường diễn ra đồng thời, nhưng điều này không phù hợp với các phương pháp hình thức
  • Các hệ thống an toàn trọng yếu như phần mềm hàng không vũ trụ có thể hưởng lợi đáng kể từ xác minh hình thức

• Lập luận rằng các phương pháp hình thức có thể giải quyết độ phức tạp của phần mềm xuất hiện khá thường xuyên

  • Điều này có thể hấp dẫn với những người ưa chuộng cách tiếp cận học thuật
  • Tuy nhiên, vẫn thiếu những trường hợp thuyết phục về cách các phương pháp hình thức thực sự giải quyết vấn đề
  • Có hàm ý rằng nếu học các công cụ như TLA thì có thể hiểu được tính hữu dụng của chúng

• Có hai loại phương pháp hình thức chính: kỹ thuật ngoại tại tách rời khỏi mã và kỹ thuật nội tại đi cùng với mã

  • Kỹ thuật nội tại hoạt động ở cấp độ chức năng của mã, còn kỹ thuật ngoại tại phân tích mô hình mã một cách hình thức
  • Hiện nay đang là thời kỳ hoàng kim của nghiên cứu về phương pháp hình thức, và các kỹ thuật nội tại đang thu hút nhiều sự chú ý hơn

• Các phương pháp hình thức hạng nhẹ có thể được duy trì cùng với codebase và cung cấp nhiều hiểu biết hơn so với kiểm thử đơn vị

  • Cách tiếp cận này phù hợp tốt với các thực hành phát triển phần mềm phổ biến

• Xác minh phần mềm hình thức vẫn là một công việc rất khó và chỉ đáng giá trong những trường hợp cực đoan

  • Nó đòi hỏi kiến thức ở cấp độ chuyên gia, và với hầu hết các hệ thống thì cực kỳ phức tạp
  • Việc học các công cụ như Lean là khó, nhưng tài liệu khá đầy đủ

• Nhiều bài viết về phương pháp hình thức tạo cảm giác như đang tạo khách hàng tiềm năng cho các tư vấn viên

  • Nên chờ cho đến khi các phương pháp hình thức thực sự tạo ra mã có chất lượng cao

• Một trong những phương pháp hình thức hạng nhẹ là xác minh truy vết bằng Linear Temporal Logic

  • Đây là một cách đơn giản nhưng mạnh mẽ để ghi lại sự kiện và thực thi các điều kiện trên dấu vết chạy

• Các phương pháp hình thức hiện đại như TLA+ và Alloy dễ học ngang với Python

  • Nhiều hệ thống đám mây đã được xác minh bằng các công cụ này (ví dụ: Azure Cosmos DB, Dynamo DB, MongoDB, CockroachDB)