ĐẠ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

• Tác giả: Trần Hoàng Việt
• Người hướng dẫn: PGS. Phạm Ngọc Hùng
• Trường học: Đại học Yale
• Chuyên ngành: Công Nghệ Thông Tin
• Đề tài: 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
• Loại tài liệu: Luận Án Tiến Sĩ
• Năm xuất bản: 2024
• Địa điểm: Hà Nội

• LỜI CAM ĐOAN
• LỜI CẢM ƠN
• TÓM TẮT
• 1. CHƯƠNG 1: CÁC ĐÓNG GÓP CHÍNH CỦA LUẬN ÁN
• 1.1. BỐ CỤC CỦA LUẬN ÁN
• 1.2. KIẾN THỨC NỀN TẢNG
• 1.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
• 1.2.2. Hệ thống chuyển trạng thái được gán nhãn
• 1.2.3. Kiểm chứng giả định - đảm bảo cho các hệ thống đặc tả bằng LTS
• 1.2.4. Đặ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 đề
• 1.2.5. Đặc tả hệ thống chuyển trạng thái bằng lôgic mệnh đề
• 1.2.6. Kiểm chứng giả định - đảm bảo cho các hệ thống đặc tả bằng lôgic mệnh đề
• 1.2.7. Đặ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
• 1.2.8. Hệ thống chuyển trạng thái có ràng buộc thời gian
• 1.2.9. Kiểm chứng giả định - đảm bảo cho các hệ thống có ràng buộc thời gian
• 1.2.10. Mô hình kiểm chứng giả định - đảm bảo
• 1.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
• 1.3.1. Các nghiên cứu liên quan
• 1.3.2. Phương pháp sinh giả định dựa trên thuật toán học L∗
• 1.3.3. Thuật toán học L∗
• 1.3.4. Thuật toán sinh giả định sử dụng thuật toán học L∗
• 1.3.5. Phương pháp sinh giả định nhỏ nhất và mạnh nhất cục bộ
• 1.3.6. Phương pháp sinh giả định mạnh nhất cục bộ
• 1.3.7. Phương pháp sinh giả định nhỏ nhất và mạnh nhất cục bộ
• 1.3.8. Thực nghiệm và thảo luận
• 1.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
• 1.4.1. Các nghiên cứu liên quan
• 1.4.2. Phương pháp sinh giả định dựa trên thuật toán CDNF
• 1.4.3. Thuật toán CDNF
• 1.4.4. Thuật toán sinh giả định dựa trên CDNF
• 1.4.5. Phương pháp sinh giả định yếu nhất cục bộ
• 1.4.6. Biến thể của thuật toán trả lời các truy vấn thành viên
• 1.4.7. Thuật toán quay lui sinh giả định yếu nhất cục bộ
• 1.4.8. Tính đúng đắn
• 1.4.9. 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
• 1.4.10. 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
• 1.4.11. Ví dụ minh họa
• 1.4.12. So sánh các thuật toán sinh giả định
• 1.4.13. Tính hiệu quả của các giả định được sinh ra trong ngữ cảnh tiến hóa
• 1.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
• 1.5.1. Các nghiên cứu liên quan
• 1.5.2. Phương pháp sinh giả định hai pha
• 1.5.3. Pha thứ nhất – pha sinh giả định không có ràng buộc thời gian
• 1.5.4. Pha thứ hai – pha sinh giả định có ràng buộc thời gian
• 1.5.5. Phiên bản một pha của phương pháp sinh giả định hai pha
• 1.5.6. Phiên bản một pha của thuật toán sinh giả định
• 1.5.7. Phiên bản cài đặt các thuật toán thực thi Teacher
• 1.5.8. Một số vấn đề trong thực tế cài đặt
• 1.5.9. Ví dụ cho quá trình sinh giả định vô hạn
• 1.5.10. Tính đúng đắn
• 1.5.11. Các kết quả đạt được
• 1.5.12. Hướng phát triển tiếp theo

I. Tổng Quan Về Kiểm Chứng Giả Định Cho Phần Mềm CBS

Trong kỷ nguyên công nghệ phần mềm hiện đại, phương pháp phần mềm dựa trên thành phần (CBS) nổi lên như một yếu tố then chốt. CBS giúp tăng hiệu quả, giảm chi phí, và rút ngắn thời gian đưa sản phẩm ra thị trường. Do đó, đảm bảo chất lượng phần mềm thành phần trở nên vô cùng quan trọng. Đối với các phần mềm quan trọng như điều khiển ô tô, tàu hỏa, máy bay, việc kiểm chứng là bắt buộc để đảm bảo các thuộc tính an toàn không bị vi phạm. Có hai hướng tiếp cận chính: chứng minh định lý (bán tự động, tốn kém) và kiểm chứng mô hình (hoàn toàn tự động). Kiểm chứng mô hình duyệt toàn bộ không gian trạng thái. Luận án này tập trung vào việc cải tiến phương pháp kiểm chứng giả định để giải quyết vấn đề bùng nổ không gian trạng thái, như đã nêu trong phần giới thiệu của luận án tiến sĩ từ Đại học Yale.

1.1. Lợi Ích của Phần Mềm Dựa Trên Thành Phần CBS

Phương pháp phần mềm dựa trên thành phần mang lại nhiều lợi ích quan trọng. Tăng hiệu quả phát triển phần mềm, giảm chi phí sản xuất. 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à nâng cấp hệ thống. CBS đã trở thành một xu hướng chủ đạo trong ngành công nghiệp phần mềm. Luận án tiến sĩ này nghiên cứu sâu hơn về cách đảm bảo chất lượng của các hệ thống CBS.

1.2. Vấn Đề Bùng Nổ Không Gian Trạng Thái Trong Kiểm Chứng Mô Hình

Kiểm chứng mô hình duyệt toàn bộ không gian trạng thái của phần mềm. Cách tiếp cận này gặp phải vấn đề bùng nổ không gian trạng thái với các hệ thống lớn. Khi hệ thống càng phức tạp, số lượng trạng thái cần kiểm tra tăng theo cấp số nhân, làm cho quá trình kiểm chứng trở nên không khả thi. Kiểm chứng giả định được đề xuất như một giải pháp để giảm thiểu vấn đề này.

II. Thách Thức Kiểm Chứng Phần Mềm Thành Phần Hiệu Quả

Mặc dù tiềm năng lớn, các nghiên cứu hiện tại cho thấy nhiều vấn đề tồn tại trong phương pháp kiểm chứng giả định. Những vấn đề này cản trở việc áp dụng rộng rãi phương pháp này trong thực tế. Luận án này đề xuất các phương pháp giải quyết một số 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ả khác nhau, như LTS và logic mệnh đề. Đồng thời, luận án xem xét ngữ cảnh tiến hóa của phần mềm, khi các thành phần thay đổi theo thời gian. Mục tiêu là cải thiện tính hiệu quả và khả năng áp dụng của phương pháp kiểm chứng giả định, như được trình bày chi tiết trong luận án tiến sĩ.

2.1. Các Loại Đặc Tả Phần Mềm Ảnh Hưởng Đến Kiểm Chứng

Phần mềm có thể đượ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 (LTS), logic mệnh đề và ô-tô-mát ghi sự kiện. Mỗi phương pháp đặc tả có ưu và nhược điểm riêng, ảnh hưởng đến quá trình kiểm chứng. Luận án này nghiên cứu các phương pháp kiểm chứng phù hợp với từng loại đặc tả, nhằm đạt được hiệu quả cao nhất.

2.2. Kiểm Chứng Phần Mềm Trong Ngữ Cảnh Tiến Hóa

Phần mềm thường xuyên trải qua quá trình tiến hóa, với các thành phần được thay đổi hoặc cập nhật. Việc kiểm chứng lại phần mềm sau mỗi lần thay đổi có thể tốn kém. Luận án này đề xuất các phương pháp giảm thiểu chi phí kiểm chứng trong ngữ cảnh tiến hóa. Bằng cách tái sử dụng các kết quả kiểm chứng trước đó và sinh ra các giả định phù hợp.

III. Cách Sinh Giả Định Nhỏ Nhất Cho Phần Mềm CBS Đặc Tả LTS

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 (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 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ự [29]. 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ộ.

3.1. Thuật Toán Học L Trong Sinh Giả Định

Thuật toán L* là một thuật toán học ngôn ngữ chính quy. Nó được sử dụng rộng rãi trong kiểm chứng giả định. Thuật toán L* tương tác với hai thực thể: Learner (người học) và Teacher (người dạy). Learner đưa ra các truy vấn, Teacher cung cấp phản hồi để Learner học được ngôn ngữ mục tiêu. Luận án này sử dụng một biến thể của thuật toán L* để sinh giả định hiệu quả hơn.

3.2. Giảm Chi Phí Tính Toán Với Giả Định Nhỏ Nhất

Việc sinh giả định có thể tốn kém về mặt tính toán. Luận án này đề xuất phương pháp sinh ra các giả định nhỏ nhất và mạnh nhất cục bộ. Các giả định này giúp giảm chi phí tính toán sinh lại giả định mới khi phần mềm tiến hóa. Đồng thời, giả định nhỏ nhất giúp giảm không gian trạng thái cần kiểm tra.

IV. Hướng Dẫn Kiểm Chứng Hồi Quy Giả Định Cho Phần Mềm Tiến Hóa

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 logic 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 hợp trong thuật toán quay lui sinh giả định yếu nhất cục bộ khi kiểm chứng. 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.

4.1. Thuật Toán CDNF Trong Kiểm Chứng Phần Mềm

Thuật toán CDNF (Conjunction of Disjunctive Normal Form) là một thuật toán học hàm logic. Được sử dụng để sinh giả định cho phần mềm đặc tả bằng logic mệnh đề. So với thuật toán L*, thuật toán CDNF có thể sinh ra các giả định nhỏ hơn và nhanh hơn trong một số trường hợp. Luận án này sử dụng thuật toán CDNF để cải thiện hiệu quả kiểm chứng.

4.2. Giảm Số Lần Sinh Lại Giả Định Trong Tiến Hóa Phần Mềm

Khi phần mềm tiến hóa, các thành phần thay đổi, có thể làm cho các giả định cũ không còn hợp lệ. Việc sinh lại giả định có thể tốn kém. Luận án này đề xuất một phương pháp sử dụng các giả định yếu nhất cục bộ. Nhằm giảm thiểu số lần sinh lại giả định trong quá trình kiểm chứng. Điều này giúp tiết kiệm thời gian và tài nguyên.

V. Thực Nghiệm Phiên Bản Một Pha Kiểm Chứng Giả Định Thời Gian

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ế. 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.

5.1. Phương Pháp Kiểm Chứng Giả Định Hai Pha

Phương pháp kiểm chứng giả định hai pha được đề xuất để xử lý các hệ thống có ràng buộc thời gian. Pha thứ nhất sinh giả định không có thời gian, pha thứ hai sinh giả định có thời gian. Luận án này đề xuất một phiên bản một pha, loại bỏ pha thứ nhất. Giúp đơn giản hóa quá trình kiểm chứng.

5.2. Kết Quả Thực Nghiệm Và Đánh Giá

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. Kết quả cho thấy phiên bản một pha có hiệu quả tương đương hoặc tốt hơn so với phiên bản hai pha trong một số trường hợp. Điều này chứng minh tính khả thi và tiềm năng của phương pháp đề xuất.

VI. Giá Trị Hướng Phát Triển Của Kiểm Chứng Phần Mềm CBS

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. Cần tiếp tục nghiên cứu để ứng dụng rộng rãi các kết quả này.

6.1. Ứng Dụng Trong Công Nghiệp Phần Mềm

Các phương pháp và công cụ được phát triển trong luận án có thể được ứng dụng trong công nghiệp phần mềm. Giúp đảm bảo chất lượng của các hệ thống phần mềm dựa trên thành phần phức tạp. Đặc biệt, các phương pháp kiểm chứng hiệu quả hơn có thể giúp giảm chi phí phát triển và bảo trì phần mềm.

6.2. Hướng Nghiên Cứu Tiếp Theo

Luận án này mở ra nhiều hướng nghiên cứu tiếp theo. Bao gồm việc mở rộng các phương pháp kiểm chứng cho các loại đặc tả phần mềm khác nhau. Phát triển các công cụ kiểm chứng tự động và hiệu quả hơn. Nghiên cứu các phương pháp kiểm chứng trong ngữ cảnh phát triển phần mềm linh hoạt (Agile).