Đặc tả hình thức - Tổng quan - Nguyễn Thị Minh Tuyền

LOGO Đặc tả hình thức Nguyễn Thị Minh Tuyền Tổng quan Nguyễn Thị Minh Tuyền 1 Đặc tả hình thức Phần mềm v Phần mềm ngày càng có ảnh hưởng lớn đến mọi mặt của cuộc sống §  Điều khiển quy trình (oil, gas, water, ) §  Giao thông vận tải (điều khiển không lưu, ) §  Chăm sóc y tế (quản lý bệnh nhân, điều khiển thiết bị, ) §  Tài chính (giao dịch tự động, bảo mật ngân hàng, ) §  Phòng thủ (điều khiển vũ khí, tên lửa, ) §  Sản xuất (lắp ráp, ) v Lỗi phần mềm không những thiệt hại về tiền của mà còn thiệt hại về cả tính mạng con người! 2 Nguyễn Thị Minh Tuyền Đặc tả hình thức Thiệt hại về tiền của do lỗi phần mềm v Hàng nghìn $ cho mỗi phút hệ thống sản xuất ngừng hoạt động. v Mất một lượng lớn tiền của và trí tuệ đầu tư cho việc sửa lỗi §  Vụ nổ Ariane 5. v Những thất bại về kinh doanh thương mại do lỗi phần mềm §  Ashton-Tate dBase. 3 Nguyễn Thị Minh Tuyền Đặc tả hình thức Lỗi phần mềm gây thiệt hại về tính mạng Những vấn đề tiềm tàng dễ thấy: v Phần mềm được dùng để điều khiển nhà máy điện hạt nhân. v Những hệ thống điều khiển không lưu. v Điều khiển phóng tàu vũ trụ. v Phần mềm nhúng trong xe hơi. v Một số ví dụ nổi tiếng: §  Các lỗi trong máy bức xạ (radiation) Therac-25. §  Lỗi khi phóng tên lửa Patriot (1991). 4 Nguyễn Thị Minh Tuyền Đặc tả hình thức Lỗi hệ thống phần mềm Những lỗi nhỏ có thể gây nên thảm họa v Vụ nổ Ariane 5 (1996) v  Lỗi phóng tên lửa chặn Patriot (1991) v Mars Climate Orbiter (1999) v London Ambulance Dispatch System v Denver Airport Luggage Handling System v Lỗi FDIV ở Intel Pentium (1994) v  5 Nguyễn Thị Minh Tuyền Đặc tả hình thức Mars Climate Orbiter 6 Nguyễn Thị Minh Tuyền Đặc tả hình thức Nguyên nhân và thiệt hại v Lỗi trong việc chuyển đổi đơn vị §  Thay vì dùng đơn vị Newtons thì lại dùng pounds v 125 triệu đô la 7 Nguyễn Thị Minh Tuyền Đặc tả hình thức Ariane 5 8 Nguyễn Thị Minh Tuyền Đặc tả hình thức Nguyên nhân và thiệt hại v Chuyển đổi từ số floating-point 64 bit thành giá trị nguyên có dấu 16 bit. v Thiệt hại 500 triệu đô la. 9 Nguyễn Thị Minh Tuyền Đặc tả hình thức Lỗi phóng tên lửa Patriot 10 Nguyễn Thị Minh Tuyền Nguồn : Đặc tả hình thức Nguyên nhân và Thiệt hại v Do sự tính toán không chính xác thời gian khởi động vì lỗi tính toán số học trên máy tính. v Đơn vị thời gian được tính bằng 1/10 giây §  Số 1/10 không được biểu diễn chính xác bằng số thực. v Chết 28 người, > 90 người bị thương 11 Nguyễn Thị Minh Tuyền Đặc tả hình thức 12 Nguyễn Thị Minh Tuyền Hours Seconds Calculated Time (sec) Inaccuracy (sec) Approx. shift in Range Gate (meters) 0 0 0 0 0 1 3600 3599.9966 .0034 7 8 28800 8799.9725 .0025 55 20(a) 72000 71999.9313 .0687 137 48 172800 172799.8352 .1648 330 72 259200 259199.7528 .2472 494 100(b) 360000 359999.6667 .3433 687 ! Đặc tả hình thức 13 Nguyễn Thị Minh Tuyền Tính toán chính xác Đặc tả hình thức 14 Nguyễn Thị Minh Tuyền Sau 8h hoạt động, sai số 20% Đặc tả hình thức 15 Nguyễn Thị Minh Tuyền Sau 100h hoạt động Đặc tả hình thức Sau khi tốt nghiệp ra trường bạn sẽ : v Đa số : xây dựng phần mềm. v Có thể bạn sẽ tham gia phát triển những hệ thống trong các lĩnh vực vừa được đề cập ở trên. v Giả sử rằng tầm quan trọng của phần mềm tăng lên: §  Bạn có thể phải chịu trách nhiệm các lỗi phần mềm. §  Công việc của bạn có thể phụ thuộc vào khả năng của bạn để tạo ra những hệ thống đáng tin cậy. Thử thách nào gặp phải khi phát triển phần mềm có độ tin cậy cao? 16 Nguyễn Thị Minh Tuyền Đặc tả hình thức Đạt được độ tin cậy trong công nghệ Một số chiến lược nổi tiếng để đạt được độ tin cậy trong các lĩnh vực công nghệ: v Ước lượng/tính toán chính xác. v Dư thừa phần cứng (“làm cho nó mạnh hơn so với mức cần thiết”) v Thiết kế mạnh (robust design). v Tách biệt rõ ràng các hệ thống con. v Thiết kế dựa vào các pattern đã được khẳng định là hoạt động tốt. 17 Nguyễn Thị Minh Tuyền Đặc tả hình thức Tại sao những điều đó không hoạt động với phần mềm? v  Hệ thống phần mềm tính toán những hàm không liên tục. v  Sự dư thừa không hỗ trợ trong việc giảm đi các lỗi phần mềm. v  Việc phát triển phần mềm dư thừa chỉ chỉ khả thi trong một số trường hợp. v  Không có sự tách biệt về vật lý hay mô hình của các hệ thống con. v  Lỗi cục bộ có thể ảnh hưởng đến toàn bộ hệ thống. v  Thiết kế phần mềm có độ phức tạp về mặt logic rất cao. v  Hầu hết các kỹ sư phần mềm không được đào tạo về tính chính xác(correctness). v  Tính hiệu quả về mặt chi phí quan trọng hơn độ tin cậy. v  Những thực tế về thiết kế phần mềm có độ tin cậy cao đang ở trạng thái nửa vời. 18 Nguyễn Thị Minh Tuyền Đặc tả hình thức Làm thế nào để đảm bảo tính chính xác của phần mềm? Inspection. Để nhiều người xem chương trình và thảo luận. v  Ưu điểm: giảm được các lỗi khó thấy trong hệ thống. v  Nhược điểm: không có cơ sở hình thức, không rõ ràng. Testing. Chạy chương trình với các đầu vào mẫu và quan sát kết quả đầu ra. v  Ưu điểm: chương trình được chỉ ra là nó hoạt động tốt trong một số trường hợp. v  Nhược điểm: §  Có thể chỉ ra sự có mặt của lỗi, nhưng không chỉ ra được sự vắng mặt của chúng. §  Làm thế nào để kiểm tra những trường hợp không mong đợi, hiếm gặp? §  Kiểm thử không thể bao phủ tất cả các trường hợp. §  Kiểm thử là “lao động chân tay”, do đó sẽ tốn kém. 19 Nguyễn Thị Minh Tuyền Đặc tả hình thức Ví dụ về kiểm thử v Một chương trình sắp xếp: public static Integer [] sort ( Integer [] a) { ... } v Kiểm thử hàm sort(): §  sort({3, 2, 5}) == {2, 3, 5} ✓ §  sort({}) == {} ✓ §  sort({17}) == {17} ✓ 20 Nguyễn Thị Minh Tuyền Đặc tả hình thức Kiểm định hình thức (Formal verification) v Bổ sung cho kiểm thử phần mềm v Kiểm định hình thức theo kiểu chứng minh định lý (Theorem Proving) Định lý: Chương trình soft() chính xác khi: v Với bất kỳ một mảng nguyên không rỗng a, hàm sort(a) trả về một mảng nguyên đã được sắp xếp, và mảng mới này là một hoán vị của a. v Phương pháp này khác với toán học: §  Biểu diễn định lý trên dưới dạng logic §  Chứng minh định lý đó với sự hỗ trợ của một automated reasoner. 21 Nguyễn Thị Minh Tuyền Đặc tả hình thức Phương pháp hình thức (Formal Method) v Là phương pháp xây dựng phần mềm dựa vào việc xem xét chương trình và việc thực thi của nó dưới dạng những đối tượng toán học và áp dụng các kỹ thuật toán học để đặc tả và phân tích các thuộc tính (property) và các hành vi (behavior) của các đối tượng. v Ưu điểm: §  Tăng độ tin cậy và tính chính xác của chương trình. §  Đặc biệt là những hệ thống cần độ an toàn cao. 22 Nguyễn Thị Minh Tuyền Đặc tả hình thức Phương pháp hình thức v Phương pháp hình thức liên quan đến hai mô tả khác nhau của cùng một hệ thống. §  Mô tả trừu tượng S, gọi là đặc tả (specification) §  Mô tả chi tiết hơn I, gọi là cài đặt (implementation) v Kiểm định (verification): §  Cho S và I, chứng tỏ rằng I là một cài đặt chính xác của S §  Hay tổng quát hơn, S và I tương thích với nhau. 23 Nguyễn Thị Minh Tuyền Đặc tả hình thức Phương pháp hình thức v Hai framework ngôn ngữ: §  Đặc tả được biểu diễn bằng ngôn ngữ đặc tả, thường được biểu diễn dưới hình thức logic hoặc khai báo tương đương. §  Cài đặt sử dụng ngôn ngữ lập trình. v Một Framework ngôn ngữ duy nhất: §  S và I được biểu diễn sử dụng cùng một ngôn ngữ. §  Khi đó, ta sẽ nói về việc thiết lập refinement, abstraction, equivalence, §  Framework này hỗ trợ quy trình phát triển nhiều bước 24 Nguyễn Thị Minh Tuyền S1 ! S2 ! ...! Sn = I Đặc tả hình thức Phương pháp hình thức v Là các phương pháp chính xác được dùng trong việc phát triển và thiết kế hệ thống. v Sử dụng logic toán học và biểu tượng (symbol) => hình thức (formal). v Tăng độ tin cậy của một hệ thống. v Hai khía cạnh §  Đặc tả hệ thống §  Cài đặt hệ thống v Có thể tạo ra mô hình hình thức (formal model) cho cả hai khía cạnh trên và sử dụng công cụ để chứng minh (prove) về mặt cơ chế rằng §  mô hình thực thi hình thức của cài đặt thỏa mãn các yêu cầu hình thức của đặc tả. 25 Nguyễn Thị Minh Tuyền Đặc tả hình thức Phương pháp hình thức v Hỗ trợ cho các phương pháp phân tích và thiết kế khác. v Là phương pháp tốt để tìm ra lỗi phần mềm (trong mã nguồn và trong đặc tả). v Giảm thời gian phát triển (và kiểm thử). v Có thể đảm bảo một số thuộc tính của mô hình hệ thống hình thức. v Chứng minh tự động sẽ là phương pháp lý tưởng. v Theorem prover 26 Nguyễn Thị Minh Tuyền Đặc tả hình thức Phương pháp hình thức và kiểm thử v Chạy hệ thống với đầu vào chọn sẵn và quan sát hành vi của nó §  Chọn ngẫu nhiên §  Chọn thông minh (bằng tay: tốn kém) §  Chọn tự động (cần đặt tả hình thức) v Những đầu vào khác thì thế nào? (test coverage) v Quan sát thì thế nào? (test oracle) Các thách thức có thể được xác định bởi các phương pháp hình thức 27 Nguyễn Thị Minh Tuyền Đặc tả hình thức Đặc tả: hệ thống nên làm gì? v Các thuộc tính đơn giản §  Các thuộc tính an toàn Những gì xấu sẽ không bao giờ xảy ra §  Những thuộc tính “sống động” Những gì tốt sẽ xảy ra sau cùng §  Các thuộc tính phi chức năng Thời gian thực, bộ nhớ, khả năng sử dụng, v Đặc tả hành vi “đầy đủ” §  Kiểm tra tính tương đương (Equivalence check) §  Lọc (Refinement) §  Tính nhất quán về dữ liệu §  28 Nguyễn Thị Minh Tuyền Đặc tả hình thức Điểm chính của phương pháp hình thức v Để chỉ ra tính chính xác (correctness) của toàn bộ hệ thống (Tính chính xác là gì? Luôn luôn đi kèm các thuộc tính cụ thể). v Để thay thế cho kiểm thử (Các phương pháp hình thức chạy trên mã nguồn, hay có thể trên byte code). v Để thay thế cho những thực tế về thiết kế. 29 Nguyễn Thị Minh Tuyền Đặc tả hình thức Lợi ích của việc sử dụng phương pháp hình thức v  Buộc người phát triển phải nghĩ về các vấn đề một cách có hệ thống. v  Cải thiện chất lượng đặc tả, thậm chí không kiểm thử hình thức. v  Đưa đến việc thiết kế tốt hơn và việc phát hiện sớm các sai sót và tính không đồng nhất. v  Cung cấp một tham chiếu chính xác (reference) để kiểm tra yêu cầu. v  Cung cấp tài liệu trong đội ngũ phát triển. v  Định hướng cho các pha phát triển tiếp theo. v  Cung cấp nền tảng cho việc tái sử dụng thông qua việc khớp đặc tả. v  Có thể thay thế nhiều test case. v  Tạo điều kiện cho việc phát sinh test case tự động. 30 Nguyễn Thị Minh Tuyền Đặc tả hình thức Đặc tả hình thức v Là cách diễn tả §  sử dụng một số ngôn ngữ hình thức và §  tại một mức trừu tượng nào đó của một tập các thuộc tính mà hệ thống phải thoả mãn. v Ngôn ngữ hình thức: §  Cú pháp có thể được xử lý một cách máy móc và được kiểm tra. §  Ngữ nghĩa được định nghĩa chặt chẽ sử dụng phương tiện toán học. v Trừu tượng: §  Trên mức mã nguồn. §  Có thể có vài mức. v Thuộc tính: §  Được biểu diễn dưới dạng logic hình thức. §  Có ngữ nghĩa rõ ràng. v Sự thoả mãn: §  Được quyết định một cách máy móc 31 Nguyễn Thị Minh Tuyền Đặc tả hình thức v Hình thức hóa đặc tả hệ thống là khó! 32 Nguyễn Thị Minh Tuyền Đặc tả hình thức Khó khăn khi tạo ra các mô hình hình thức 33 Nguyễn Thị Minh Tuyền Đặc tả hình thức Khó khăn khi tạo ra các mô hình hình thức 34 Nguyễn Thị Minh Tuyền Đặc tả hình thức v Việc chứng minh các thuộc tính của hệ thống có thể là một thử thách. 35 Nguyễn Thị Minh Tuyền Đặc tả hình thức Lịch sử v  Những năm 80, kiểm định phần mềm được xem như “chết”. §  Ít tự động, người lập trình phải nỗ lực “bằng chân tay” quá nhiều. §  Chỉ có một số ít chương trình ví dụ có thể chạy được. v  Những năm 90, kiểm tra mô hình (model checkers) thành công. §  Kiểm tra một cách đầy đủ và tự động hoàn toàn các mô hình (trạng thái hữu hạn). §  Kiểm định phần cứng và các giao thức giao tiếp. v  Từ cuối những năm 90, mối quan tâm về kiểm định phần mềm tăng lên. §  Chứng minh/kiểm tra mô hình những phần quan trọng của phần mềm. v  Những ứng dụng mới như proof-carrying-code (PCC). §  Đặt mã máy (machine code) cùng với proof và chứng minh rằng mã máy đó thỏa mãn một số thuộc tính về bảo mật/an toàn. v  Những vấn đề mới chẳng hạn xem xét về vấn đề bảo mật. Phương pháp hình thức là chủ để “hot” trong nghiên cứu cũng như trong công nghiệp 36 Nguyễn Thị Minh Tuyền Đặc tả hình thức Ngôn ngữ và hệ thống Các ngôn ngữ đặc tả v  Ngôn ngữ tổng quát: VDM (Vienna Development Method), Z, ASM (Abstract State Machines), OCL (Object Constraint Language for UML), . . . v  Ngôn ngữ gắn với ngôn ngữ lập trình: SPARK (Ada), Larch/C++, JML v  (Java), Spec#(C#), ACSL (C), . . . v  Algebraic/axiomatic: OBJ, ACT One, Larch, CASL, . . . v  Concurrent: Unity, Estelle, Lotos, TLA, . . . v  Mobile: pi-Calculus, . . . Kiểm tra mô hình (Model Checker) v  Spin, SMV, BLAST, Bandera, SLAM, VeriSoft, . . . Hỗ trợ việc chứng minh (Proving Assistant) v  PVS, HOL, Isabelle, Coq, Theorema, . . . Môi trường kiểm định v  Edinburgh Concurrency Workbench, STeP (Stanford Temporal Prover), KIV (Karlsruhe Interactive Verifier), JIVE (Java Interactive Verification Environment), LOOP, Krakatoa/Why, KeY, Mobius, . . . 37 Nguyễn Thị Minh Tuyền Đặc tả hình thức Pp hình thức trong công nghiệp v Đường metro 14 ở Paris §  Dự án Méteor. §  Hoàn toàn tự động. §  Phần quan trọng về độ an toàn của hệ thống này được phát triển và thẩm định sử dụng B-Method. §  Tìm ra được rất nhiều lỗi trong quá trình chứng minh. v Airport shuttle ở sân bay Roissy Charles de Gaulle (Paris) §  B-Method. v Hệ thống tàu lửa ở Đan Mạch §  Sử dụng phương pháp hình thức RAISE để mô hình hóa hệ thống kiểm tra những thuộc tính về an toàn. v  v  38 Nguyễn Thị Minh Tuyền Đặc tả hình thức Tổng kết v Phần mềm ngày càng phổ biến và phức tạp. v Các kỹ thuật phát triển hiện tại là không đầy đủ. v Phương pháp hình thức §  Không phải là “phương thuốc chữa bách bệnh” nhưng ngày càng cần thiết. §  Ngày càng được ứng dụng nhiều trong thực tế. §  Thời gian phát triển phần mềm ngắn hơn. §  Tăng chất lượng sản phẩm. v Trong môn này, chúng ta sẽ học vài phương pháp hình thức khác nhau, cho các giai đoạn phát triển phần mềm khác nhau. 39 Nguyễn Thị Minh Tuyền LOGO