Luận á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

ĐẠI HỌC YALE 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 LUẬN ÁN TIẾN SĨ NGÀNH CÔNG NGHỆ THÔNG TIN Hà Nội – 2024 ĐẠI HỌC YALE 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 Chuyên ngành: Kỹ thuật Phần mềm Mã số: 9480103.01 LUẬN ÁN TIẾN SĨ NGÀNH CÔNG NGHỆ THÔNG TIN NGƯỜI HƯỚNG DẪN KHOA HỌC: 1.Kiều Mai Chi 2. Võ Đình Chiến Hà Nội – 2024 Mục lục Chương 1. Các đóng góp chính của luận án. Bố cục của luận án.

KIẾN THỨC NỀN TẢNG. Đặc tả và kiểm chứng giả định - đảm bảo cho các hệ thống đặc tả bằng LTS. Hệ thống chuyển trạng thái được gán nhãn. Kiểm chứng giả định - đảm bảo cho các hệ thống đặc tả bằng LTS.

Đặ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 đề. Đặc tả hệ thống chuyển trạng thái bằng lôgic mệnh đề. Kiểm chứng giả định - đảm bảo cho các hệ thống đặc tả bằng lôgic mệnh đề. Đặ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.

Hệ thống chuyển trạng thái có ràng buộc thời gian. Kiểm chứng giả định - đảm bảo cho các hệ thống có ràng buộc thời gian. Mô hình kiểm chứng giả định - đảm bảo. 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.

Các nghiên cứu liên quan. Phương pháp sinh giả định dựa trên thuật toán học L∗. Thuật toán học L∗. Thuật toán sinh giả định sử dụng thuật toán học L∗.

Phương pháp sinh giả định nhỏ nhất và mạnh nhất cục bộ. Phương pháp sinh giả định mạnh nhất cục bộ. Phương pháp sinh giả định nhỏ nhất và mạnh nhất cục bộ. Thực nghiệm và thảo luận.

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. Các nghiên cứu liên quan. Phương pháp sinh giả định dựa trên thuật toán CDNF. Thuật toán CDNF.

Thuật toán sinh giả định dựa trên CDNF. Phương pháp sinh giả định yếu nhất cục bộ. Biến thể của thuật toán trả lời các truy vấn thành viên. Thuật toán quay lui sinh giả định yếu nhất cục bộ.

Tính đúng đắn. 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. 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í dụ minh họa.

So sánh các thuật toán sinh giả định. Tính hiệu quả của các giả định được sinh ra trong ngữ cảnh tiến hóa 98 4. 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. Các nghiên cứu liên quan.

Phương pháp sinh giả định hai pha. Pha thứ nhất – pha sinh giả định không có ràng buộc thời gian 109 5. Pha thứ hai – pha sinh giả định có ràng buộc thời gian. Phiên bản một pha của phương pháp sinh giả định hai pha.

Phiên bản một pha của thuật toán sinh giả định. Phiên bản cài đặt các thuật toán thực thi Teacher. Một số vấn đề trong thực tế cài đặt. Ví dụ cho quá trình sinh giả định vô hạn.

Tính đúng đắn. Các kết quả đạt được. 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.1 Mô hình kiểm chứng giả định - đảm bảo.1 Tương tác giữa L∗ Learner và T eacher.2 Quá trình kiểm chứng thành phần tại bước thứ i.3 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.4 Mối quan hệ giữa s, L(A), and L(AW ).5 Ý 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∗ .6 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.7 Ý tưởng để tính tempQ, comF inalState, và Cikj .8 Ý tưởng của phương pháp sinh giả định nhỏ nhất và mạnh nhất cục bộ.1 Thuật toán CBAG.2 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.3 Mối quan hệ giữa L(AO ), L(AN ), và L(AW ).4 Mối quan hệ giữa ListN W và ListN .5 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.6 Thuật toán sinh lại giả định cho CBS trong ngữ cảnh tiến hóa.1 Phương pháp sinh giả định hai pha.2 Ví dụ về quá trình sinh giả định lặp vô hạn.3 Ứng viên cho giả định tương ứng.

119 iv Danh sách bảng 2.1 Các phép gán cho ví dụ về chuỗi .1 Kết quả thực nghiệm so sánh Thuật toán 3.1 và Thuật toán 3.2 Kết quả thực nghiệm so sánh Thuật toán 3.1 và Thuật toán 3.3 Không gian trạng thái giảm được với giả định được sinh bởi Thuật toán 3.1 Bảng chân lý của phép toán lôgic kéo theo .2 Sinh giả định đầu tiên sử dụng thuật toán LWAG .3 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 .4 So sánh các phương pháp sinh giả định .5 So sánh các phương pháp sinh lại giả định .1 Một bảng quan sát trong quá trình kiểm chứng M .2 Kết quả thực nghiệm phiên bản một pha. 123 v Thuật ngữ và từ viết tắt Từ viết Giải nghĩa - Từ gốc tắt tạm dịch AG Assume-Guarantee Giả định - đảm bảo Assume-Guarantee AGV Kiểm chứng giả định - đảm bảo Verification AMC Adaptive Model Checking Kiểm chứng mô hình thích nghi Thuật toán sinh giả định dựa trên thuật CBAG CDNF-based assumption generation toán CDNF CBS Component-based software Phần mềm dựa trên thành phần Conjunction of Disjunctive Normal Tên một thuật toán học hàm lôgic CDNF Form dùng để sinh giả định Kiểm chứng giả định - đảm bảo quay CIRC-AG Circular Assume-Guarantee vòng CNF Conjunctive Normal Form Dạng chuẩn hội DFA Deterministic Finite State Automata Ô-tô-mát hữu hạn trạng thái đơn định DNF Disjunctive Normal Form Dạng chuẩn tuyển EQ Equivalence query Thuật toán trả lời truy vấn ứng viên ERA Event-Recording Automaton Ô-tô-mát ghi sự kiện FMS Flexible Manufacturing System Hệ thống sản xuất linh hoạt GSS Gas station system Hệ thống trạm gas Thuật toán trả lời truy vấn thành viên IMQ Improved membership query cải tiến IW Is witness Thuật toán phân tích phản ví dụ Locally minimum and strongest Công cụ sinh giả định nhỏ nhất và mạnh LMAG assumption generation tool nhất cục bộ Locally strongest assumption LSAG Công cụ sinh giả định mạnh nhất cục bộ generation tool LTS Labelled transition system 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ệ LTSA Labelled transition system analyser thống chuyển trạng thái được gán nhãn LWAG Local weakest assumption generation Thuật toán sinh giả định yếu nhất cục bộ MTBDD Multiterminal binary decision diagram Sơ đồ quyết định nhị phân đa chiều Kiểm chứng giả định - đảm bảo không NC-AG Non-circular assume-guarantee quay vòng Thuật toán trả lời truy vấn thành viên OMQ Original membership query ban đầu Tên một công cụ đặc tả, kiểm chứng PAT Process Analysis Toolkit phần mềm Công cụ kiểm chứng phần mềm có ràng Tivet Timed systems verification tool buộc thời gian vi 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. 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. 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.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ự.