Tài liệu Một số cải tiến phương pháp kiểm chứng giả định – đảm bảo cho phần mềm dựa trên thành phần.

Mục lục Chương 1. GIỚI THIỆU. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.1. Đặt vấn đề . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.2. Các đóng góp chính của luận án . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.3. Bố cục của luận án . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1 6 8 Chương 2. KIẾN THỨC NỀN TẢNG . . . . . . . . . . . . . . . . . . . . . . . . . . 9 2.1. Đặc tả và kiểm chứng giả định - đảm bảo cho các hệ thống đặc tả bằng LTS. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 2.1.1. Hệ thống chuyển trạng thái được gán nhãn. . . . . . . . . . . . . . . . . . . . . . 9 2.1.2. Kiểm chứng giả định - đảm bảo cho các hệ thống đặc tả bằng LTS . 13 2.2. Đặc tả và kiểm chứng giả định - đảm bảo cho các hệ thống đặc tả bằng lôgic mệnh đề . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 2.2.1. Đặc tả hệ thống chuyển trạng thái bằng lôgic mệnh đề . . . . . . . . . 16 2.2.2. Kiểm chứng giả định - đảm bảo cho các hệ thống đặc tả bằng lôgic mệnh đề . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 2.3. Đặc tả và kiểm chứng giả định - đảm bảo cho các hệ thống có ràng buộc thời gian . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 2.3.1. Hệ thống chuyển trạng thái có ràng buộc thời gian . . . . . . . . . . . . . 21 2.3.2. Kiểm chứng giả định - đảm bảo cho các hệ thống có ràng buộc thời gian . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 2.4. Mô hình kiểm chứng giả định - đảm bảo . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 2.5. Tổng kết. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Chương 3. PHƯƠNG PHÁP SINH GIẢ ĐỊNH NHỎ NHẤT VÀ MẠNH NHẤT CỤC BỘ CHO VIỆC KIỂM CHỨNG PHẦN MỀM DỰA TRÊN THÀNH PHẦN . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 3.1. Giới thiệu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 3.2. Các nghiên cứu liên quan . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 3.3. Phương pháp sinh giả định dựa trên thuật toán học L∗ . . . . . . . . . . . . 33 3.3.1. Thuật toán học L∗ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 i 3.3.2. Thuật toán sinh giả định sử dụng thuật toán học L∗ . . . . . . . . . . . 3.4. Phương pháp sinh giả định nhỏ nhất và mạnh nhất cục bộ . . . . . . . . . 3.4.1. Phương pháp sinh giả định mạnh nhất cục bộ. . . . . . . . . . . . . . . . . . 3.4.2. Phương pháp sinh giả định nhỏ nhất và mạnh nhất cục bộ . . . . . 3.5. Thực nghiệm và thảo luận . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.6. Tổng kết. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 36 37 45 55 65 Chương 4. PHƯƠNG PHÁP KIỂM CHỨNG HỒI QUY GIẢ ĐỊNH - ĐẢM BẢO CHO PHẦN MỀM TIẾN HÓA . . . . . . . . . . . . . . . . . . 67 4.1. Giới thiệu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 4.2. Các nghiên cứu liên quan . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70 4.3. Phương pháp sinh giả định dựa trên thuật toán CDNF. . . . . . . . . . . . . 73 4.3.1. Thuật toán CDNF . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73 4.3.2. Thuật toán sinh giả định dựa trên CDNF . . . . . . . . . . . . . . . . . . . . . . 74 4.4. Phương pháp sinh giả định yếu nhất cục bộ . . . . . . . . . . . . . . . . . . . . . . . . 78 4.4.1. Biến thể của thuật toán trả lời các truy vấn thành viên . . . . . . . . 78 4.4.2. Thuật toán quay lui sinh giả định yếu nhất cục bộ . . . . . . . . . . . . . 80 4.4.3. Tính đúng đắn . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82 4.5. Phương pháp kiểm chứng từng phần cho phần mềm dựa trên thành phần trong ngữ cảnh tiến hóa. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 88 4.5.1. Phương pháp kiểm chứng giả định - đảm bảo cho phần mềm trong ngữ cảnh tiến hóa . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90 4.5.2. Ví dụ minh họa . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91 4.6. Thực nghiệm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94 4.6.1. So sánh các thuật toán sinh giả định . . . . . . . . . . . . . . . . . . . . . . . . . . . 94 4.6.2. Tính hiệu quả của các giả định được sinh ra trong ngữ cảnh tiến hóa 98 4.6.3. Thảo luận . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102 4.7. Tổng kết . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104 Chương 5. THỬ NGHIỆM CÀI ĐẶT PHIÊN BẢN MỘT PHA CHO VIỆC KIỂM CHỨNG GIẢ ĐỊNH - ĐẢM BẢO CHO PHẦN MỀM CÓ RÀNG BUỘC THỜI GIAN . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 106 5.1. Giới thiệu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 106 5.2. Các nghiên cứu liên quan . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108 5.3. Phương pháp sinh giả định hai pha . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108 5.3.1. Pha thứ nhất – pha sinh giả định không có ràng buộc thời gian 109 5.3.2. Pha thứ hai – pha sinh giả định có ràng buộc thời gian . . . . . . . 110 ii 5.4. Phiên bản một pha của phương pháp sinh giả định hai pha . . . . . . . 5.4.1. Phiên bản một pha của thuật toán sinh giả định . . . . . . . . . . . . . . 5.4.2. Phiên bản cài đặt các thuật toán thực thi Teacher . . . . . . . . . . . . 5.5. Thảo luận . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.5.1. Một số vấn đề trong thực tế cài đặt . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.5.2. Ví dụ cho quá trình sinh giả định vô hạn . . . . . . . . . . . . . . . . . . . . . 5.6. Tính đúng đắn . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.7. Thực nghiệm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.8. Tổng kết . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 111 111 113 116 116 118 119 121 124 Chương 6. KẾT LUẬN . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 126 6.1. Các kết quả đạt được . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 126 6.2. Hướng phát triển tiếp theo . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 128 iii Danh sách hình vẽ 1.1 Tổng quan về phương pháp kiểm chứng giả định - đảm bảo và các vấn đề còn tồn tại. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 2.1 Mô hình kiểm chứng giả định - đảm bảo. . . . . . . . . . . . . . . . . 26 3.1 3.2 3.3 3.7 Tương tác giữa L∗ Learner và T eacher. . . . . . . . . . . . . . . . Quá trình kiểm chứng thành phần tại bước thứ i. . . . . . . . . Một phản ví dụ cho thấy các giả định được sinh bởi phương pháp của Cobleigh và cộng sự [29] không phải là mạnh nhất. . . . . . Mối quan hệ giữa s, L(A), and L(AW ). . . . . . . . . . . . . . . . Ý tưởng chính của phương pháp sinh giả định mạnh nhất cục bộ dựa vào L∗ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Ví dụ cho sự tồn tại của một giả định nhỏ hơn và mạnh hơn (ALM S ) giả định được sinh bởi Thuật toán 3.1 (A). . . . . . . . . Ý tưởng để tính tempQ, comF inalState, và Cikj . . . . . . . . . . . 3.8 Ý tưởng của phương pháp sinh giả định nhỏ nhất và mạnh nhất cục bộ.53 4.1 4.2 4.6 Thuật toán CBAG. . . . . . . . . . . . . . . . . . . . . . . . . . . Thuật toán LWAG sinh giả định yếu nhất cục bộ cho việc kiểm chứng giả định - đảm bảo cho các CBS. . . . . . . . . . . . . . . Mối quan hệ giữa L(AO ), L(AN ), và L(AW ). . . . . . . . . . . . . Mối quan hệ giữa ListN W và ListN . . . . . . . . . . . . . . . . . . Sử dụng lại giả định được sinh bởi thuật toán LWAG cho việc kiểm chứng CBS trong ngữ cảnh tiến hóa. . . . . . . . . . . . . . Thuật toán sinh lại giả định cho CBS trong ngữ cảnh tiến hóa. . 5.1 5.2 5.3 Phương pháp sinh giả định hai pha. . . . . . . . . . . . . . . . . . . . 109 Ví dụ về quá trình sinh giả định lặp vô hạn. . . . . . . . . . . . . . . . 119 Ứng viên cho giả định tương ứng. . . . . . . . . . . . . . . . . . . . . . 119 3.4 3.5 3.6 4.3 4.4 4.5 iv . . . 33 . . . 35 . . . 37 . . . 38 . . . 44 . . . 46 . . . 47 . . . 77 . . . 80 . . . 86 . . . 87 . . . 89 . . . 91 Danh sách bảng 2.1 Các phép gán cho ví dụ về chuỗi . . . . . . . . . . . . . . . . . . . . . 18 3.1 3.2 3.3 Kết quả thực nghiệm so sánh Thuật toán 3.1 và Thuật toán 3.3 . . . 56 Kết quả thực nghiệm so sánh Thuật toán 3.1 và Thuật toán 3.4 . . . 59 Không gian trạng thái giảm được với giả định được sinh bởi Thuật toán 3.4 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60 4.1 4.2 4.3 4.4 4.5 Bảng chân lý của phép toán lôgic kéo theo . . . . . . . . . . . . . Sinh giả định đầu tiên sử dụng thuật toán LWAG . . . . . . . . Sinh giả định cho hệ thống trong ngữ cảnh tiến hóa sử dụng thuật toán LWAG và phương pháp kiểm chứng đề xuất . . . . . . . . . So sánh các phương pháp sinh giả định . . . . . . . . . . . . . . . So sánh các phương pháp sinh lại giả định . . . . . . . . . . . . . 5.1 5.2 Một bảng quan sát trong quá trình kiểm chứng M . . . . . . . . . . . 118 Kết quả thực nghiệm phiên bản một pha . . . . . . . . . . . . . . . . 123 v . . . 79 . . . 92 . . . 93 . . . 98 . . . 101 Thuật ngữ và từ viết tắt Từ viết tắt AG Giải nghĩa tạm dịch Giả định - đảm bảo Từ gốc AMC Assume-Guarantee Assume-Guarantee Verification Adaptive Model Checking CBAG CDNF-based assumption generation CBS Component-based software Conjunction of Disjunctive Normal Form AGV Kiểm chứng giả định - đảm bảo CIRC-AG Circular Assume-Guarantee CNF Conjunctive Normal Form Kiểm chứng mô hình thích nghi Thuật toán sinh giả định dựa trên thuật toán CDNF Phần mềm dựa trên thành phần Tên một thuật toán học hàm lôgic dùng để sinh giả định Kiểm chứng giả định - đảm bảo quay vòng Dạng chuẩn hội DFA DNF EQ Deterministic Finite State Automata Disjunctive Normal Form Equivalence query Ô-tô-mát hữu hạn trạng thái đơn định Dạng chuẩn tuyển Thuật toán trả lời truy vấn ứng viên ERA FMS GSS Event-Recording Automaton Flexible Manufacturing System Gas station system IMQ Improved membership query IW LTS Is witness Locally minimum and strongest assumption generation tool Locally strongest assumption generation tool Labelled transition system Ô-tô-mát ghi sự kiện Hệ thống sản xuất linh hoạt Hệ thống trạm gas Thuật toán trả lời truy vấn thành viên cải tiến Thuật toán phân tích phản ví dụ Công cụ sinh giả định nhỏ nhất và mạnh nhất cục bộ LTSA Labelled transition system analyser LWAG MTBDD Local weakest assumption generation Multiterminal binary decision diagram NC-AG Non-circular assume-guarantee OMQ Original membership query PAT Process Analysis Toolkit Tivet Timed systems verification tool CDNF LMAG LSAG Công cụ sinh giả định mạnh nhất cục bộ vi Hệ thống chuyển trạng thái được gán nhãn Công cụ hỗ trợ đặc tả và kiểm chứng hệ thống chuyển trạng thái được gán nhãn Thuật toán sinh giả định yếu nhất cục bộ Sơ đồ quyết định nhị phân đa chiều Kiểm chứng giả định - đảm bảo không quay vòng Thuật toán trả lời truy vấn thành viên ban đầu Tên một công cụ đặc tả, kiểm chứng phần mềm Công cụ kiểm chứng phần mềm có ràng buộc thời gian Lời cam đoan Tôi xin cam đoan đây là công trình nghiên cứu do tôi thực hiện dưới sự hướng dẫn của thầy giáo, PGS. TS. Phạm Ngọc Hùng và thầy giáo, TS. Võ Đình Hiếu tại Bộ môn Công nghệ Phần mềm, Khoa Công nghệ Thông tin, Trường Đại học Công nghệ, Đại học Quốc gia Hà Nội. Các số liệu và kết quả trình bày trong luận án là trung thực, chưa được công bố bởi bất kỳ tác giả nào hay ở bất kỳ công trình nào khác. Tác giả Trần Hoàng Việt vii Lời cảm ơn Trước tiên tôi xin gửi lời cảm ơn chân thành và sâu sắc đến thầy giáo, PGS. TS. Phạm Ngọc Hùng và thầy giáo, TS. Võ Đình Hiếu – những người đã hướng dẫn, khuyến khích, truyền cảm hứng, chỉ bảo và tạo cho tôi những điều kiện tốt nhất từ khi bắt đầu làm nghiên cứu sinh đến khi hoàn thành luận án này. Tôi xin chân thành cảm ơn các thầy cô giáo khoa Công nghệ thông tin, Trường Đại Học Công Nghệ, Đại Học Quốc Gia Hà Nội, đặc biệt là các Thầy Cô trong Bộ môn Công Nghệ Phần Mềm đã tận tình đào tạo, cung cấp cho tôi những kiến thức vô cùng quý giá, đã tạo điều kiện tốt nhất cho tôi về môi trường làm việc trong suốt quá trình học tập, nghiên cứu tại Trường. Tôi xin trân trọng cảm ơn đề tài mã số 102.03-2015.25 được tài trợ bởi Quỹ phát triển khoa học và công nghệ quốc gia (NAFOSTED) đã hỗ trợ tôi trong quá trình thực hiện luận án. Cuối cùng, tôi xin chân thành cảm ơn những người thân trong gia đình cùng toàn thể bạn bè đã luôn giúp đỡ, động viên tôi những lúc gặp phải khó khăn trong suốt quá trình học tập và nghiên cứu. viii Tóm tắt Kiểm chứng giả định - đảm bảo được biết đến như là một trong những giải pháp quan trọng nhằm giải quyết bài toán bùng nổ không gian trạng thái trong kiểm chứng mô hình cho các hệ thống phần mềm dựa trên thành phần. Ý tưởng chính của phương pháp này là kiểm chứng từng phần nhỏ của phần mềm mà không cần ghép chúng. Mặc dù có tiềm năng áp dụng lớn trong thực tế, các nghiên cứu hiện tại cho thấy nhiều vấn đề còn tồn tại của phương pháp này ngăn cản nó được áp dụng rộng rãi. Luận án đề xuất phương pháp giải quyết một số trong các vấn đề đó của quá trình kiểm chứng cho phần mềm được đặc tả bằng nhiều loại đặc tả và trong ngữ cảnh tiến hóa. Cụ thể, luận án đã đạt được ba kết quả chính như sau. Luận án đề xuất phương pháp sinh giả định nhỏ nhất và mạnh nhất cục bộ cho bài toán kiểm chứng giả định - đảm bảo các phần mềm dựa trên thành phần đặc tả bằng hệ chuyển trạng thái được gán nhãn (Labelled Transition System LTS). Các giả định này góp phần giảm chi phí tính toán sinh lại giả định mới và giảm không gian trạng thái khi kiểm chứng các phần mềm tiến hóa. Ý tưởng chính của phương pháp là sử dụng một biến thể của phương pháp trả lời các truy vấn thành viên được đề xuất bởi Cobleigh và cộng sự. Biến thể này được tích hợp trong thuật toán đề xuất để sinh được các giả định nhỏ nhất và mạnh nhất cục bộ. Các chứng minh cho tính đúng đắn của phương pháp đề xuất cũng được trình bày trong luận án. Một công cụ hỗ trợ đã được xây dựng và tiến hành thực nghiệm với các hệ thống ban đầu cho những kết quả khả quan so với các phương pháp hiện có. Luận án đề xuất phương pháp sinh giả định yếu nhất cục bộ và phương pháp sử dụng các giả định đó để giảm số lần sinh lại giả định khi kiểm chứng giả định - đảm bảo phần mềm được đặc tả bằng lôgic mệnh đề trong ngữ cảnh tiến hóa. Để làm việc này, luận án đề xuất một biến thể của thuật toán trả lời các truy vấn thành viên được đề xuất bởi Chen và cộng sự. Biến thể này được tích ix hợp trong thuật toán quay lui sinh giả định yếu nhất cục bộ khi kiểm chứng. Biến thể của phương pháp trả lời truy vấn thành viên và thuật toán quay lui này được tích hợp trong phương pháp đề xuất nhằm giảm được tối đa số lần giả định cần được sinh lại khi kiểm chứng phần mềm tiến hóa. Việc này giúp giảm chi phí cho quá trình kiểm chứng các phần mềm trong ngữ cảnh tiến hóa phần mềm. Tính đúng đắn của thuật toán đề xuất cũng được chứng minh trong luận án. Công cụ hỗ trợ cho phương pháp đã được cài đặt và tiến hành thực nghiệm với các hệ thống phổ biến trong cộng đồng nghiên cứu và cho những kết quả tốt so với các phương pháp hiện nay. Luận án thực nghiệm cài đặt phiên bản một pha cho phương pháp kiểm chứng giả định - đảm bảo hai pha được đề xuất bởi Lin và cộng sự cho phần mềm dựa trên thành phần có ràng buộc thời gian. Phiên bản này loại bỏ pha sinh giả định không có thời gian từ quá trình kiểm chứng. Luận án cũng trình bày một số vấn đề phát sinh và phương pháp xử lý trong quá trình cài đặt phương pháp kiểm chứng trong thực tế. Tính đúng đắn của phiên bản đề xuất được trình bày và thảo luận trong luận án. Công cụ hỗ trợ đã được cài đặt và thực nghiệm với một số hệ thống phổ biến trong cộng đồng nghiên cứu và cho các kết quả khả quan. Các đề xuất của luận án đóng góp các giải pháp về mặt lý thuyết và công cụ hỗ trợ nhằm nâng cao hiệu quả của phương pháp kiểm chứng giả định - đảm bảo góp phần làm cho các phương pháp kiểm chứng mô hình dễ dàng được áp dụng hơn trong thực tiễn. Luận án góp phần nâng cao chất lượng trong công nghiệp phần mềm nói chung và trong cộng đồng nghiên cứu nói riêng. x Chương 1 GIỚI THIỆU 1.1. Đặt vấn đề Trong ba thập kỷ vừa qua, công nghệ phần mềm dựa trên thành phần (Component-Based Software Engineering - CBSE) nổi lên như một cách tiếp cận quan trọng trong công nghệ phần mềm vì các đặc tính cả về nghiệp vụ và kỹ thuật của nó như: tăng hiệu quả, giảm chi phí, rút ngắn thời gian đưa sản phẩm ra thị trường, tăng khả năng bảo trì, v.v. [99]. Từ đó, việc đảm bảo chất lượng cho các phần mềm dựa trên thành phần (Component-Based Software CBS) đóng vai trò sống còn trong vòng đời phát triển của chúng do yêu cầu ngày càng tăng về chất lượng. Với các sản phẩm phần mềm quan trọng có yêu cầu chất lượng cao như các phần mềm điều khiển ô tô, tàu hỏa, máy bay, v.v., các phần mềm này được yêu cầu thỏa mãn một số thuộc tính (thuộc tính được nghiên cứu trong luận án này là thuộc tính an toàn) cho trước, kiểm chứng là bắt buộc để đảm bảo thuộc tính đã cho không bị vi phạm trong toàn bộ thời gian hoạt động của chúng. Có hai hướng tiếp cận chính nhằm giải quyết vấn đề này gồm: hướng tiếp cận chứng minh định lý (theorem proving) là hướng tiếp cận bán tự động, đòi hỏi có sự tham gia của các chuyên gia trong quá trình kiểm chứng [31, 35, 53, 60, 61, 95], cần nhiều công sức và chi phí [9] và hướng tiếp cận kiểm chứng mô hình (model checking) là hướng tiếp cận hoàn toàn tự động [12]. Trong hai hướng tiếp cận này, hướng tiếp cận kiểm chứng mô hình [24, 25, 27, 54, 90] nhận được sự quan tâm đặc biệt trong cộng đồng nghiên cứu và trong công nghiệp phần mềm vì tính tự động hoàn toàn của nó. Kiểm chứng mô hình là hướng tiếp cận vét cạn thông qua việc duyệt qua toàn bộ không gian trạng thái của phần mềm để kiểm tra xem phần mềm có vi phạm thuộc tính 1 đã cho hay không. Nếu không có sự vi phạm nào, hệ thống ban đầu thỏa mãn thuộc tính đã cho. Ngược lại, một minh chứng về sự vi phạm sẽ được trả lại. Vì đặc tính vét cạn không gian trạng thái của hệ thống cần kiểm chứng, hướng tiếp cận này gặp vấn đề về sự bùng nổ không gian trạng thái đối với các hệ thống lớn [24, 26, 90]. Để tận dụng được những ưu điểm của kiểm chứng mô hình và giải quyết vấn đề về bùng nổ không gian trạng thái, phương pháp kiểm chứng giả định - đảm bảo (Assume-Guarantee Verification - AGV) đã được đề xuất [23, 44, 52, 81, 88]. Kiểm chứng giả định-đảm bảo là phương pháp kiểm chứng dựa trên chiến lược chia để trị. Trong đó, hệ thống phần mềm lớn được chia thành các thành phần nhỏ hơn để kiểm chứng. Từ đó, quá trình kiểm chứng kết luận rằng hệ thống tổng thể có thỏa mãn thuộc tính đã cho hay không mà không phải ghép nối toàn bộ các thành phần lại với nhau. Trong phương pháp kiểm chứng giả định - đảm bảo, có hai phương pháp lập luận: giả định - đảm bảo quay vòng (Circular Assume - Guarantee Reasoning CIRC-AG) [3, 64, 75, 77, 78, 84] và giả định - đảm bảo không quay vòng (NonCircular Assume - Guarantee Reasoning - NC-AG) [5, 21, 23, 41, 44, 68, 76, 96]. Trong luận án này, thuật ngữ “kiểm chứng giả định - đảm bảo quay vòng” và “kiểm chứng giả định - đảm bảo không quay vòng” được sử dụng lần lượt để chỉ “phương pháp kiểm chứng sử dụng lập luận quay vòng” và “phương pháp kiểm chứng sử dụng lập luận không quay vòng”. Sau này, phương pháp kiểm chứng giả định - đảm bảo không quay vòng được mở rộng, áp dụng cho các hệ thống được đặc tả bằng nhiều phương pháp khác nhau như: hệ chuyển trạng thái được gán nhãn (Labelled Transition Systems - LTS) [18, 22, 29, 41, 45, 46, 55, 56, 57, 58, 86], hệ thống có ràng buộc thời gian (timed systems) [68, 69], hệ thống chuyển trạng thái được đặc tả bằng lôgic mệnh đề [21, 48, 94], hệ thống chuyển trạng thái tượng trưng (symbolic transition systems) [6, 49, 82, 83], các hệ thống có yếu tố xác suất (probalistic systems) [16, 20, 37, 62], v.v. Bài toán quan trọng nhất trong phương pháp kiểm chứng giả định - đảm bảo là làm sao để sinh được giả định. Để giải quyết vấn đề này, các phương pháp hiện nay đều dựa vào các thuật toán học ngôn ngữ chính quy thông qua sự tương tác của hai thực thể Learner và T eacher. Tùy vào loại hệ thống (có hoặc không có ràng buộc thời gian) và tùy vào phương pháp đặc tả được sử dụng (đặc tả bằng hệ chuyển trạng thái được gán nhãn, lôgic mệnh đề, và ô-tô-mát ghi sự kiện, v.v.), thuật toán sinh giả định sẽ được lựa chọn tương ứng (L∗ [8, 91], và 2 CDNF (Conjunction of Disjunctive Normal Form) [15, 21], T L∗ [68, 69], v.v.). Mặc dù tồn tại nhiều phương pháp kiểm chứng giả định - đảm bảo, các phương pháp này đều có những ưu và nhược điểm nhất định. Tổng quan về phương pháp kiểm chứng giả định - đảm bảo và các vấn đề còn tồn tại được trình bày trong Hình 1.1. Trong luận án này, phần mềm được đặc tả bằng các dạng đặc tả khác nhau như LTS, lôgic mệnh đề, và ô-tô-mát ghi sự kiện và thuộc tính được kiểm chứng là thuộc tính an toàn. Kiểm chứng M’ hiệu quả? Tăng tốc độ kiểm chứng? Mô hình phần mềm tiến hóa · Yes + giả định A · No + phản ví dụ cex Mô hình phần mềm LTS Lôgic mệnh đề ERA Kiểm chứng M với các loại đặc tả khác nhau? Bùng nổ không gian trạng thái? Hình 1.1: Tổng quan về phương pháp kiểm chứng giả định - đảm bảo và các vấn đề còn tồn tại. Phương pháp kiểm chứng giả định - đảm bảo cho hệ thống chuyển trạng thái được gán nhãn là phương pháp phổ biến nhất trong cộng đồng nghiên cứu cũng như trong việc áp dụng trong công nghiệp. Trong phương pháp này, các luật kiểm chứng giả định - đảm bảo cho thấy rằng bản chất của bài toán kiểm chứng là bài toán bao của các ngôn ngữ và độ phức tạp của quá trình kiểm chứng tỉ lệ thuận với số trạng thái của giả định được sinh ra [100]. Theo đó, chi phí của quá trình kiểm chứng (chi phí được đề cập trong luận án này là chi phí về thời gian), đặc biệt trong ngữ cảnh tiến hóa (từ phần mềm M thành M 0 ), có thể nhỏ hơn nếu sử dụng giả định có số trạng thái và ngôn ngữ nhỏ hơn. Để sinh giả định cho bài toán kiểm chứng giả định - đảm bảo cho các hệ thống được đặc tả bằng LTS, Giannakopoulou và cộng sự là nhóm tác giả đầu tiên chỉ ra sự tồn tại của giả định yếu nhất (giả định có ngôn ngữ lớn nhất) trong kiểm chứng giả định - đảm bảo [41, 87]. Tiếp đó, Cobleigh và cộng sự đề xuất sử dụng thuật toán L∗ [8, 91] sinh giả định cho bài toán kiểm chứng giả định - đảm bảo [29]. Sau Cobleigh, có nhiều nghiên cứu mở rộng, cải tiến, tối ưu 3 cũng như áp dụng kết quả của Cobleigh cho nhiều ngữ cảnh khác của việc kiểm chứng phần mềm [10, 39, 87, 22, 28, 93, 17, 18, 19, 46, 38, 101, 86, 55, 57, 58]. Mặc dù vậy, vẫn chưa có nghiên cứu nào đề xuất phương pháp sinh giả định nhỏ nhất và mạnh nhất để giảm chi phí kiểm chứng phần mềm trong ngữ cảnh tiến hóa (tăng hiệu quả, tốc độ kiểm chứng M 0 ). Phương pháp kiểm chứng giả định - đảm bảo sử dụng đặc tả bằng LTS là phương pháp phổ biến và thường được áp dụng cho các hệ thống được đặc tả ở mức cao, như mức thiết kế, dưới dạng các hệ thống chuyển trạng thái. Tuy nhiên, độ phức tạp của nó vẫn rất cao. Vì vậy, trường hợp hệ thống được đặc tả ở mức thấp hơn dưới dạng lôgic mệnh đề, một số nghiên cứu khác đã sử dụng phương pháp kiểm chứng được đề xuất bởi Chen và cộng sự để giảm độ phức tạp của quá trình kiểm chứng [21, 48]. Các thuật toán kiểm chứng giả định đảm bảo sử dụng đặc tả bằng lôgic mệnh đề có những ưu điểm vượt trội so với các thuật toán sử dụng đặc tả bằng ô-tô-mát. Thứ nhất, về khả năng biểu diễn, đặc tả bằng lôgic mệnh đề tương đương với đặc tả bằng ô-tô-mát không đơn định và nó có thể biểu diễn súc tích hơn nhiều lần so với đặc tả bằng ô-tô-mát. Do đó, các thuật toán kiểm chứng sử dụng đặc tả bằng lôgic mệnh đề sinh các giả định có số trạng thái ít hơn nhiều lần các giả định sinh bởi các phương pháp sử dụng thuật toán L∗ . Thứ hai, xét về tốc độ thì thuật toán sinh giả định sử dụng đặc tả bằng lôgic mệnh đề sử dụng các thuật toán như CDNF [15], v.v. có tốc độ tốt hơn các thuật toán kiểm chứng sử dụng thuật toán L∗ [21]. Năm 2007, Sinha và cộng sự đã đề xuất sử dụng bộ giải nhằm kiểm tra tính thỏa mãn của hàm lôgic (SAT solver) cho bài toán kiểm chứng giả định - đảm bảo với các hệ thống được đặc tả bằng lôgic mệnh đề [94]. Năm 2010, Chen và cộng sự đã đề xuất áp dụng thuật toán CDNF được đề xuất bởi Bshouty [15] cho bài toán kiểm chứng giả định - đảm bảo cho hệ thống chuyển trạng thái được đặc tả bằng lôgic mệnh đề [21]. Sau Chen, năm 2016, He và cộng sự đã đề xuất một phương pháp sinh giả định có tốc độ nhanh và hiệu quả sử dụng thuật toán CDNF để sinh các giả định trong quá trình kiểm chứng giả định - đảm bảo cho hệ thống phần mềm được đặc tả bằng lôgic mệnh đề [48]. Sau đó, phương pháp này được áp dụng cho việc kiểm chứng hồi quy cho phần mềm tiến hóa. Tuy nhiên, trong ngữ cảnh tiến hóa phần mềm, thuật toán vẫn cần sinh lại giả định trong tất cả các trường hợp dù chỉ có sự thay đổi nhỏ trong các thành phần của phần mềm ban đầu. 4 Trong phát triển phần mềm nói chung, ngoài các phần mềm không có ràng buộc thời gian được đặc tả bằng LTS hoặc lôgic mệnh đề, v.v, các hệ thống có ràng buộc thời gian cũng nhận được sự quan tâm đặc biệt của cộng đồng nghiên cứu và trong công nghiệp. Do đó, việc kiểm chứng các phần mềm này trở thành một xu hướng tất yếu do các đòi hỏi về chất lượng của các hệ thống thời gian thực ngày càng cao và trong nhiều lĩnh vực của đời sống xã hội như Internet vạn vật, khoa học vũ trụ, v.v. Một trong các phương pháp đặc tả các hệ thống có ràng buộc thời gian là sử dụng các ô-tô-mát ghi sự kiện (Event - Recording Automata - ERA) [4]. Năm 2010, Grinchtein và cộng sự đề xuất thuật toán học T L∗sg để học các ô-tô-mát ghi sự kiện [42]. Sau đó, năm 2014, Lin và cộng sự là nhóm tác giả đầu tiên đề xuất bài toán kiểm chứng giả định - đảm bảo cho phần mềm có ràng buộc thời gian được đặc tả bằng ô-tô-mát ghi sự kiện [68]. Phương pháp được Lin đề xuất sử dụng thuật toán học ô-tô-mát ghi sự kiện T L∗ cũng được đề xuất bởi cùng nhóm tác giả năm 2011 [69]. Thuật toán này được phát triển từ thuật toán T L∗sg được đề xuất trước đó bởi Grinchtein và cộng sự [42]. Thuật toán T L∗ được triển khai vào bộ công cụ hỗ trợ việc kiểm chứng hệ thống có ràng buộc thời gian gọi là PAT [71, 97]. Tuy phương pháp của Lin có thể sinh được giả định cho bài toán kiểm chứng giả định - đảm bảo cho phần mềm có ràng buộc thời gian, phương pháp này có độ phức tạp cao nên vẫn rất khó khăn để có thể được áp dụng rộng rãi trong cộng đồng nghiên cứu và trong công nghiệp. Từ các phân tích trên, luận án hướng tới các mục tiêu sau. Mục tiêu thứ nhất là sinh giả định nhỏ nhất và mạnh nhất cho bài toán kiểm chứng giả định - đảm bảo. Mục tiêu này hướng tới việc giảm chi phí thời gian khi sinh lại giả định trong quá trình kiểm chứng phần mềm đã tiến hóa. Mục tiêu thứ hai là giảm chi phí thời gian của quá trình kiểm chứng giả định - đảm bảo phần mềm đã tiến hóa bằng cách giảm số lần sinh lại giả định khi kiểm chứng hồi quy. Luận án đề xuất phương pháp sinh giả định yếu nhất cục bộ cho quá trình kiểm chứng giả định - đảm bảo. Các giả định này được sử dụng trong phương pháp đề xuất để giảm số lần sinh lại giả định khi kiểm chứng hồi quy phần mềm tiến hóa. Mục tiêu cuối cùng của luận án là tiến hành thử nghiệm cài đặt phiên bản một pha của phương pháp kiểm chứng giả định - đảm bảo hai pha cho phần mềm có ràng buộc thời gian. Để đạt được mục tiêu này, luận án tiến hành nghiên cứu, cài đặt, và xử lý các vấn đề phát sinh trong quá trình cài đặt phương pháp sinh 5 giả định được đề xuất bởi Lin và cộng sự [68]. Đối tượng nghiên cứu của luận án là phương pháp kiểm chứng giả định - đảm bảo cho phần mềm dựa trên thành phần. Trong khuôn khổ luận án này, phương pháp kiểm chứng giả định - đảm bảo cho các phần mềm tương tranh không có và có ràng buộc thời gian lần lượt được đặc tả bằng ba loại đặc tả là LTS, lôgic mệnh đề, và ERA được nghiên cứu và cải tiến. Các loại đặc tả này quyết định các phương pháp kiểm chứng tương ứng được sử dụng là phương pháp sử dụng thuật toán L∗ [29], phương pháp kiểm chứng sử dụng thuật toán CDNF [21], và thuật toán T L∗ [68]. Tuy nhiên, các phương pháp kiểm chứng giả định - đảm bảo hiện có cho phần mềm sử dụng ba loại đặc tả này vẫn chưa phải là tối ưu về chi phí thời gian và chưa được áp dụng trong ngữ cảnh tiến hóa phần mềm. Do đó, luận án tập trung vào tối ưu chi phí thời gian cho các phương pháp kiểm chứng này và trong ngữ cảnh tiến hóa. Các nghiên cứu này có ý nghĩa lớn trong việc nâng cao chất lượng phần mềm và làm cho phương pháp kiểm chứng giả định - đảm bảo được áp dụng rộng rãi hơn trong thực tiễn. Để đạt được mục tiêu nghiên cứu, các phương pháp kiểm chứng giả định đảm bảo đã có sẽ được tiến hành khảo sát. Từ đó, các khoảng trống nghiên cứu được xác định làm cơ sở để đề xuất các phương pháp mới hoặc cải tiến các phương pháp hiện có. Các công cụ hỗ trợ thực nghiệm cũng được xây dựng để minh chứng cho tính đúng đắn và tính hiệu quả của các đề xuất và cải tiến. 1.2. Các đóng góp chính của luận án Luận án đạt được ba kết quả chính gồm: (i) phương pháp sinh giả định nhỏ nhất và mạnh nhất cho việc kiểm chứng phần mềm dựa trên thành phần, (ii) phương pháp kiểm chứng hồi quy giả định - đảm bảo cho phần mềm tiến hóa, (iii) kết quả thử nghiệm cài đặt phiên bản một pha cho phương pháp kiểm chứng giả định - đảm bảo hai pha cho phần mềm có ràng buộc thời gian. Chi tiết các đóng góp của luận án như sau. Đề xuất một phương pháp sinh các giả định nhỏ nhất và mạnh nhất cục bộ cho bài toán kiểm chứng giả định - đảm bảo cho phần mềm dựa trên thành phần. Các giả định này góp phần làm giảm chi phí tính toán khi kiểm chứng phần mềm đã tiến hóa do độ phức tạp của quá trình kiểm chứng tỉ lệ thuận với độ lớn của ngôn ngữ của các thành phần phần mềm và số trạng thái của chúng. 6 Tính đúng đắn của phương pháp đề xuất cũng được chứng minh trong luận án. Một công cụ hỗ trợ cũng đã được cài đặt và thực nghiệm với một số ví dụ điển hình để minh chứng cho tính hiệu quả của phương pháp đề xuất. Đề xuất một phương pháp kiểm chứng hồi quy giả định - đảm bảo một cách hiệu quả bằng cách giảm số lần cần sinh lại giả định khi kiểm chứng cho phần mềm trong ngữ cảnh tiến hóa. Phương pháp này dựa trên thuật toán quay lui đề xuất nhằm sinh các giả định yếu nhất cục bộ khi kiểm chứng. Các chứng minh cho tính đúng đắn của phương pháp đề xuất cũng được trình bày trong luận án. Một công cụ hỗ trợ cũng đã được cài đặt và thực nghiệm với một số hệ thống phổ biến trong cộng đồng nghiên cứu và cho những kết quả khả quan. Tiến hành thử nghiệm cài đặt phiên bản một pha cho phương pháp kiểm chứng giả định - đảm bảo hai pha cho hệ thống phần mềm có ràng buộc thời gian. Thử nghiệm này nhằm có được đánh giá về thời gian, hiệu quả của quá trình kiểm chứng một pha. Một số trường hợp phát sinh trong quá trình cài đặt và phương pháp xử lý cũng được trình bày trong luận án. Trường hợp đầu tiên là trường hợp Teacher “không biết” nếu tiếp tục quá trình kiểm chứng có thể sinh được giả định cần tìm không hoặc trường hợp Teacher “không biết” trả về phản ví dụ nào để Learner tiếp tục quá sinh các ứng viên giả định tốt hơn. Trường hợp thứ hai là hiện thực hóa việc trả về các phản ví dụ cho Learner của Teacher và việc phân tích các phản ví dụ này ở phía Learner để sinh các giả định tốt hơn ở bước kiểm chứng tiếp theo. Tính đúng đắn của các đề xuất cũng được trình bày và thảo luận trong luận án. Một công cụ đã được cài đặt và tiến hành thực nghiệm với một số hệ thống phổ biến và cho kết quả tốt. Các kết quả nghiên cứu trên cải tiến phương pháp kiểm chứng giả định - đảm bảo cho phần mềm dựa trên thành phần được đặc tả bằng nhiều loại đặc tả khác nhau. Tùy vào loại đặc tả mà đội phát triển phần mềm sử dụng, cải tiến tương ứng có thể được lựa chọn. Khi các phần mềm được mô hình hóa ở mức cao dưới dạng các hệ thống chuyển trạng thái, cải tiến ở Chương 3 nên được sử dụng. Ngược lại, khi quá trình kiểm chứng đòi hỏi tốc độ cao và các hệ thống được mô hình hóa ở mức thấp hơn, đội phát triển nên áp dụng cải tiến ở Chương 4. Ngoài ra, khi phát triển các phần mềm có ràng buộc thời gian, các phần mềm này nên được đặc tả bằng ERA để có thể áp dụng các thử nghiệm trong Chương 5. Các đóng góp này góp phần làm cho phương pháp kiểm chứng giả định - đảm bảo trở nên hiệu quả và được sử dụng nhiều hơn trong phát triển phần mềm. Từ 7 đó, chất lượng phần mềm ngày càng được nâng cao và đảm bảo nhằm đáp ứng được đòi hỏi ngày càng cao của cộng đồng nghiên cứu nói riêng cũng như trong công nghiệp phần mềm nói chung. 1.3. Bố cục của luận án Phần còn lại của luận án được cấu trúc như sau. Chương 2 giới thiệu các khái niệm cơ bản được sử dụng trong các nghiên cứu của luận án. Trong chương này, các phương pháp đặc tả và kiểm chứng cho các hệ thống phần mềm được trình bày. Các phương pháp đặc tả này bao gồm LTS, lôgic mệnh đề, và ERA. Phương pháp sinh giả định nhỏ nhất và mạnh nhất cục bộ được trình bày trong Chương 3 sử dụng đặc tả bằng LTS. Chương 4 đề xuất một phương pháp sinh giả định yếu nhất cục bộ và sử dụng giả định đó trong việc kiểm chứng các phần mềm trong ngữ cảnh tiến hóa. Lôgic mệnh đề được sử dụng để đặc tả các hệ thống phần mềm trong nghiên cứu của chương này. Một thử nghiệm cài đặt phiên bản một pha cho phương pháp kiểm chứng giả định - đảm bảo hai pha cho phần mềm có ràng buộc thời gian được giới thiệu trong Chương 5. Trong chương này, các thành phần phần mềm và thuộc tính của chúng được đặc tả bằng ERA. Cuối cùng, tổng kết các kết quả nghiên cứu của luận án và các hướng nghiên cứu tiếp theo được trình bày trong Chương 6. 8 Chương 2 KIẾN THỨC NỀN TẢNG Chương này trình bày các khái niệm nền tảng và các phương pháp kiểm chứng được sử dụng trong luận án. Các khái niệm cơ bản gồm các phương pháp đặc tả phần mềm sử dụng các hệ thống chuyển trạng thái được gán nhãn, lôgic mệnh đề, ô-tô-mát ghi sự kiện, v.v. Các phương pháp kiểm chứng giả định - đảm bảo sử dụng các loại đặc tả trên và các khái niệm liên quan cũng được giới thiệu. 2.1. Đặc tả và kiểm chứng giả định - đảm bảo cho các hệ thống đặc tả bằng LTS 2.1.1. Hệ thống chuyển trạng thái được gán nhãn Các hệ thống chuyển trạng thái được gán nhãn (Labelled Transition Systems - LTS) được dùng để đặc tả các hành vi của các thành phần phần mềm cũng như các thuộc tính của chúng. Các nghiên cứu trong Chương 3 và Chương 5 của luận án sẽ sử dụng các khái niệm này. Gọi Act là tập các hành vi toàn cục quan sát được của phần mềm và τ là một hành vi cục bộ không quan sát được của thành phần nhìn từ góc nhìn của môi trường của thành phần. π được dùng để biểu diễn một trạng thái đặc biệt gọi là trạng thái lỗi. Một LTS được định nghĩa như sau. Định nghĩa 2.1 (LTS). Một LTS M là một bộ gồm bốn thành phần ký hiệu là hQ, Σ, δ, q0 i, trong đó: • Q là một tập không rỗng các trạng thái, • Σ ⊆ Act là một tập hữu hạn các hành vi quan sát được gọi là bảng chữ cái của M , 9 • δ ⊆ Q × Σ ∪ {τ } × Q là quan hệ chuyển trạng thái, và • q0 ∈ Q là trạng thái khởi tạo. Chú ý 2.1 Số lượng trạng thái của M được gọi là kích thước của M , ký hiệu là |M | (|M | = |Q|). Đây là một khái niệm có ảnh hưởng lớn đến độ phức tạp của các thuật toán kiểm chứng nói chung và trong các thuật toán đề xuất trong Chương 3 nói riêng. Chuỗi được dùng để biểu diễn một dãy có thứ tự các hành vi quan sát được của phần mềm. Đây là khái niệm được sử dụng xuyên suốt trong luận án. Đối với phần mềm được đặc tả bằng một LTS M , một chuỗi của M được định nghĩa như sau. Định nghĩa 2.2 (Chuỗi). Một chuỗi σ của một LTS M = hQ, Σ, δ, q0 i là một trình tự hữu hạn các hành vi a1 a2 ...an , mà tồn tại một trình tự các trạng thái bắt đầu từ trạng thái khởi tạo (nghĩa là tồn tại q0 q1 ...qn ), với 1 ≤ i ≤ n, sao cho (qi−1 , ai , qi ) ∈ δ , qi ∈ Q. Trong quá trình làm việc với các phần mềm được đặc tả bằng LTS, đặc biệt là trong các thuật toán sinh giả định được trình bày trong Chương 3 và Chương 5, các ngôn ngữ của chúng là tập các chuỗi thường xuyên được đề cập tới. Trong các phép toán về ngôn ngữ, phép ghép nối là một trong những phép toán quan trọng nhất. Định nghĩa 2.3 (Phép ghép nối). Cho hai tập các chuỗi hành vi P ⊆ Σ∗ và Q ⊆ Σ∗ , phép ghép nối của P và Q được định nghĩa là P.Q = {pq | p ∈ P, q ∈ Q}, trong đó pq biểu diễn phép ghép nối của các chuỗi p và q . Chú ý 2.2 Tập hợp tất cả các chuỗi của M được gọi là ngôn ngữ của M , ký hiệu là L(M ). Gọi σ = a1 a2 ...an là một chuỗi của một LTS M . Ký hiệu [σ ] được dùng để biểu diễn một LTS Mσ = hQ, Σ, δ, q0 i, trong đó Q = {q0 , q1 , ..., qn }, và δ = {(qi−1 , ai , qi )}, với 1 ≤ i ≤ n. Chương 3 và Chương 4 nghiên cứu cải tiến các phương pháp kiểm chứng giả định - đảm bảo cho phần mềm trong ngữ cảnh tiến hóa. Vì vậy, khái niệm tiến hóa là một khái niệm quan trọng được sử dụng trong các chương này cũng như trong toàn bộ luận án. Trong thực tế phát triển phần mềm, khái niệm này được hiểu theo các cách khác nhau tùy thuộc vào ngữ cảnh sử dụng của nó. Trong 10