Các phương pháp chính thức của việc xác minh chương trình có một vị trí trong ngành không?

Question

Tôi đã xem qua số Hoare Logic ở trường đại học. Những gì chúng tôi đã làm thật sự đơn giản. Hầu hết những gì tôi đã làm là chứng minh tính chính xác của các chương trình đơn giản bao gồm các vòng lặp while, if và chuỗi hướng dẫn nhưng không có gì khác. Những phương pháp này có vẻ rất hữu ích!

Các phương pháp chính thức có được sử dụng rộng rãi trong ngành không?

Những phương pháp này có được sử dụng để chứng minh phần mềm quan trọng không?

Answer 1

Đây là câu hỏi gần gũi với trái tim tôi (tôi là nhà nghiên cứu trong Xác minh phần mềm bằng cách sử dụng logic chính thức), vì vậy bạn sẽ không ngạc nhiên khi tôi nói rằng các kỹ thuật này có một địa điểm hữu ích và chưa sử dụng đủ trong ngành.

Có rất nhiều cấp độ "phương pháp chính thức", vì vậy tôi giả sử bạn có nghĩa là những người nghỉ ngơi trên cơ sở toán học khắt khe (trái ngược với, nói theo một số quy trình 6-Sigma). Một số loại phương pháp chính thức đã có thành công lớn - hệ thống kiểu là một ví dụ. Các công cụ phân tích tĩnh dựa trên phân tích lưu lượng dữ liệu cũng phổ biến, việc kiểm tra mô hình gần như phổ biến trong thiết kế phần cứng, và các mô hình tính toán như Pi-Calculus và CCS dường như đang truyền cảm hứng cho một số thay đổi thực sự trong thiết kế ngôn ngữ thực tế. Phân tích chấm dứt là một trong đó đã có rất nhiều báo chí gần đây - Dự án SDV tại Microsoft và làm việc của Byron Cook là những ví dụ gần đây về nghiên cứu/thực hành chéo trong các phương pháp chính thức.

Hoare Reasoning đã không, cho đến nay, đã xâm nhập lớn trong ngành - vì nhiều lý do hơn tôi có thể liệt kê, nhưng tôi nghi ngờ chủ yếu là về sự phức tạp của văn bản. lớn và không thể hiện thuộc tính của nhiều môi trường thế giới thực). Các tiểu lĩnh vực khác nhau trong loại lý luận này hiện đang xâm nhập lớn vào những vấn đề này - Tách logic là một.

Đây là một phần bản chất của nghiên cứu đang diễn ra (khó). Nhưng tôi phải thú nhận rằng chúng tôi, như các nhà lý thuyết, hoàn toàn thất bại trong việc giáo dục ngành về lý do tại sao các kỹ thuật của chúng tôi hữu ích, giữ cho chúng phù hợp với nhu cầu của ngành và làm cho chúng dễ tiếp cận với các nhà phát triển phần mềm. Ở một mức độ nào đó, đó không phải là vấn đề của chúng tôi - chúng tôi là các nhà nghiên cứu, thường là các nhà toán học và sử dụng thực tế không phải là quan trọng nhất trong tâm trí của chúng tôi. Ngoài ra, các kỹ thuật được phát triển thường quá phôi để sử dụng trong các hệ thống quy mô lớn - chúng tôi làm việc trên các chương trình nhỏ, trên các hệ thống đơn giản, giúp toán học hoạt động và tiếp tục. Mặc dù vậy, tôi không mua nhiều lý do này - chúng ta nên tích cực hơn trong việc thúc đẩy ý tưởng của mình và nhận được phản hồi giữa ngành và công việc của chúng tôi (một trong những lý do chính tôi quay lại nghiên cứu).

Đây có thể là một ý tưởng tốt cho tôi để hồi sinh weblog của tôi, và làm cho một số bài viết thêm về công cụ này ...

Answer 2

"Các phương pháp chính thức được sử dụng trong ngành?"

Có.

Tuyên bố assert bằng nhiều ngôn ngữ lập trình có liên quan đến các phương pháp chính thức để xác minh chương trình.

"Các phương pháp chính thức được sử dụng trong ngành rộng rãi?"

No.

"Những phương pháp này được sử dụng để chứng minh phần mềm quan trọng?"

Đôi khi. Thường xuyên hơn, chúng được sử dụng để chứng minh rằng phần mềm là an toàn. Chính thức hơn, chúng được sử dụng để chứng minh một số xác nhận liên quan đến bảo mật nhất định về phần mềm.

Answer 3

Vâng, Sir Tony Hoare đã tham gia nghiên cứu của Microsoft khoảng 10 năm trước và một trong những điều ông bắt đầu là xác minh chính thức hạt nhân Windows NT. Thật vậy, đây là một trong những lý do cho sự chậm trễ lâu dài của Windows Vista: bắt đầu với Vista, phần lớn hạt nhân là thực sự đã được xác minh chính thức. Điều này chắc chắn không phải là điển hình, nhưng nó có lẽ là ứng dụng quan trọng nhất của việc xác minh chương trình chính thức, về tác động của nó (sau khi tất cả, gần như mọi con người). là một cách nào đó, hình dạng hoặc hình thức bị ảnh hưởng bởi một máy tính đang chạy Windows).

Answer 4

Có, chúng được sử dụng, nhưng không rộng rãi trong mọi lĩnh vực. Có nhiều phương pháp hơn là chỉ hoare logic, một số được sử dụng nhiều hơn, một số ít hơn, tùy thuộc vào sự phù hợp cho nhiệm vụ nhất định. Vấn đề thường gặp là phần mềm là biiiiiiig và xác minh rằng tất cả đều chính xác vẫn là một vấn đề quá khó.

Ví dụ: định lý-prover (phần mềm hỗ trợ con người trong việc chứng minh tính chính xác của chương trình) ACL2 đã được sử dụng để chứng minh rằng một đơn vị xử lý dấu phẩy động không có loại lỗi nào đó. Đó là một nhiệm vụ lớn, vì vậy kỹ thuật này không quá phổ biến.

Kiểm tra mẫu, một loại xác minh chính thức khác, được sử dụng khá phổ biến hiện nay, ví dụ: Microsoft cung cấp một loại trình kiểm tra mô hình trong bộ phát triển trình điều khiển và có thể được sử dụng để xác minh trình điều khiển cho một bộ lỗi phổ biến. Bộ kiểm tra mô hình cũng thường được sử dụng trong việc xác minh mạch phần cứng.

Kiểm tra nghiêm ngặt cũng có thể được coi là xác minh chính thức - có một số đặc điểm chính thức về đường dẫn chương trình nào cần được kiểm tra và v.v.

Answer 5

Polyspace là một (hideously đắt tiền, nhưng rất tốt) Sản phẩm thương mại dựa trên xác minh chương trình. Nó khá thực dụng, trong đó nó tăng lên từ 'thử nghiệm đơn vị nâng cao có thể sẽ tìm thấy một số lỗi' trong 'ba năm tiếp theo của cuộc đời bạn sẽ được chi cho thấy 10 tệp này không có khuyết điểm'.

Nó dựa trên xác minh tiêu cực ('chương trình này sẽ không làm hỏng ngăn xếp của bạn') thay vì xác minh tích cực ('chương trình này sẽ làm chính xác những gì 50 trang của phương trình nói nó sẽ').

Answer 6

Tôi không thể nhận xét nhiều về phần mềm nhiệm vụ quan trọng, mặc dù tôi biết rằng ngành công nghiệp điện tử sử dụng nhiều kỹ thuật để xác thực phần mềm, bao gồm các phương pháp kiểu Hoare.

Phương pháp chính thức đã phải chịu đựng bởi vì những người ủng hộ sớm như Edsger Dijkstra khẳng định rằng họ nên được sử dụng ở khắp mọi nơi. Cả các hình thức và sự hỗ trợ của phần mềm đều không làm được. Những người ủng hộ hợp lý hơn tin rằng những phương pháp này nên được sử dụng cho những vấn đề khó khăn. Chúng không được sử dụng rộng rãi trong công nghiệp, nhưng việc áp dụng ngày càng tăng. Có lẽ sự xâm nhập lớn nhất đã được sử dụng các phương pháp chính thức để kiểm tra các thuộc tính an toàn an toàn của phần mềm. Một số ví dụ yêu thích của tôi là kiểm tra mô hình SPIN và mã mang theo bằng chứng của George Necula.

Di chuyển khỏi thực tiễn và nghiên cứu, dự án hệ điều hành Singularity của Microsoft là sử dụng các phương pháp chính thức để cung cấp đảm bảo an toàn thường yêu cầu hỗ trợ phần cứng. Điều này dẫn đến hiệu suất nhanh hơn và đảm bảo mạnh mẽ hơn.Ví dụ, trong kỳ dị, họ đã chứng minh rằng nếu trình điều khiển thiết bị của bên thứ ba được cho phép vào hệ thống (có nghĩa là điều kiện xác minh cơ bản đã được chứng minh), thì nó không thể làm giảm toàn bộ hệ điều hành đó. thiết bị của riêng mình.

Phương pháp chính thức chưa được sử dụng rộng rãi trong công nghiệp, nhưng chúng được sử dụng rộng rãi hơn 20 năm trước và 20 năm kể từ bây giờ chúng sẽ được sử dụng rộng rãi hơn. Vì vậy, bạn được tương lai-proofed :-)

Answer 7

Để thêm vào của Jorg answer, đây là một interview với Tony Hoare. Các công cụ mà Jorg đề cập đến, tôi nghĩ, là PREfast và Tiền tố. Xem here để biết thêm thông tin.

Answer 8

Có hai cách tiếp cận khác nhau đối với các phương pháp chính thức trong ngành.

Một cách tiếp cận là thay đổi hoàn toàn quy trình phát triển. Ký hiệu Z và phương thức B được đề cập trong danh mục đầu tiên này. B đã được áp dụng cho sự phát triển của dòng tàu điện ngầm không người lái 14 ở Paris (nếu bạn có cơ hội, trèo lên toa xe phía trước. Thường thì bạn không có cơ hội nhìn thấy đường ray phía trước bạn).

Cách tiếp cận khác, tăng dần hơn là duy trì các quy trình xác minh và phát triển hiện có và chỉ thay thế một trong các tác vụ xác minh tại một thời điểm bằng một phương pháp mới. Điều này rất hấp dẫn nhưng nó có nghĩa là phát triển các công cụ phân tích tĩnh để thoát, các ngôn ngữ được sử dụng thường không dễ phân tích (vì chúng không được thiết kế để). Nếu bạn đi đến (ví dụ)

http://dblp.uni-trier.de/db/indices/a-tree/d/Delmas:David.html

(xin lỗi, chỉ có một siêu liên kết cho phép người dùng mới :()

bạn sẽ tìm thấy trường hợp của các ứng dụng thực tiễn của phương pháp chính thức để xác minh C các chương trình (với các máy phân tích tĩnh Astrée, Caveat, Fluctuat, Frama-C) và mã nhị phân (với các công cụ từ AbsInt GmbH)

Nhân tiện, vì bạn đã đề cập Hoare Logic, trong danh sách các công cụ trên, chỉ Caveat là dựa trên logic Hoare (và Frama-C có một plug-in logic Hoare). ely về giải thích trừu tượng, một kỹ thuật khác với cách tiếp cận tự động hơn.

Answer 9

Bên cạnh các cách tiếp cận thủ tục hơn khác, Hoare logic đã được trong cơ sở Design by Contract, giới thiệu như là một kỹ thuật hướng đối tượng bởi Bertrand Meyer trong Eiffel (see Meyer's article of 1992, trang 4). Mặc dù Thiết kế theo Hợp đồng không giống như phương pháp xác minh chính thức (một điều, DbC không chứng minh bất kỳ thứ gì cho đến khi phần mềm được thực hiện), theo ý kiến ​​của tôi, nó cung cấp một cách sử dụng thực tế hơn.

Answer 10

Lĩnh vực chuyên môn của tôi là sử dụng các phương pháp chính thức để phân tích mã tĩnh để cho thấy phần mềm đó không có lỗi thời gian chạy. Điều này được thực hiện bằng cách sử dụng một phương pháp chính thức được gọi là "giải thích trừu tượng". Kỹ thuật này cho phép bạn chứng minh một số thuộc tính của chương trình s/w. Ví dụ. chứng minh rằng a + b sẽ không tràn hoặc x/(x-y) sẽ không dẫn đến chia cho 0. Một công cụ phân tích tĩnh ví dụ sử dụng kỹ thuật này là Polyspace.

Đối với câu hỏi của bạn: "Các phương pháp chính thức có được sử dụng rộng rãi trong ngành không?" và "Những phương pháp này có được sử dụng để chứng minh phần mềm quan trọng không?"

Câu trả lời là có.Ý kiến ​​này dựa trên kinh nghiệm của tôi và hỗ trợ công cụ Polyspace cho các ngành dựa vào việc sử dụng phần mềm nhúng để kiểm soát các hệ thống an toàn quan trọng như ga điện tử trong ô tô, hệ thống phanh cho tàu hỏa, bộ điều khiển động cơ phản lực, bơm truyền thuốc, Các ngành công nghiệp này thực sự sử dụng các loại công cụ phương thức chính thức này.

Tôi không tin rằng tất cả 100% các phân đoạn ngành này đang sử dụng các công cụ này, nhưng việc sử dụng ngày càng tăng. Ý kiến ​​của tôi là ngành công nghiệp hàng không vũ trụ và ô tô dẫn đầu với ngành công nghiệp thiết bị y tế nhanh chóng tăng cường sử dụng.