Luận văn thạc sĩ khoa học máy tính sinh test case tự động cho chương trình chứa điều kiện phức tạp sử dụng giải thuật di truyền

Luận văn thạc sĩ nghiên cứu phương pháp sinh test case tự động cho chương trình phức tạp bằng giải thuật di truyền, ứng dụng hiệu quả trong kiểm thử phần mềm.

• Tác giả: Nguyễn Cát Định
• Người hướng dẫn: TS. Quản Thành Thơ
• Trường học: Đại học Bách Khoa - Đại học Quốc gia TP.HCM
• Chuyên ngành: Khoa học máy tính
• Đề tài: Sinh test case tự động cho chương trình chứa điều kiện phức tạp sử dụng giải thuật di truyền
• Loại tài liệu: luận văn thạc sĩ
• Năm xuất bản: 2012
• Địa điểm: TP. Hồ Chí Minh

Mục lục chi tiết

• LỜI CẢM ƠN
• LỜI CAM ĐOAN
• MỤC LỤC HÌNH
• MỤC LỤC BẢNG
• MỞ ĐẦU
• 1. CHƯƠNG 1: TỔNG QUAN
• 1.1. Phát biểu đề tài
• 1.2. Đóng góp của đề tài
• 1.3. Bố cục của luận văn
• 1.4. Tính đúng đắn của chương trình (Program Correctness)
• 1.4.1. Kiểm tra phần mềm (Software Verification)
• 1.4.2. Kiểm thử phần mềm (Software Testing)
• 1.4.3. Thực thi kí hiệu (Symbolic Execution)
• 1.5. Các giải thuật hướng tự nhiên
• 1.5.1. Mô phỏng luyện kim (Simulated Annealing)
• 1.5.2. Giải thuật di truyền (Genetic Algorithm)
• 1.6. Các phương pháp sinh test case tự động
• 1.6.1. Phương pháp hướng mục tiêu (Goal-oriented)
• 1.6.2. Phương pháp hướng đường đi (Path-oriented)
• 1.6.3. Những phương pháp sinh test case khác
• 2. CHƯƠNG 2: PHƯƠNG PHÁP SINH TEST CASE CHO CHƯƠNG TRÌNH
• 2.1. Chương trình chứa điều kiện phức tạp
• 2.2. Phương pháp đề xuất
• 2.3. Bộ phân tích mã nguồn (Code Analyzer)
• 2.4. Bộ thực thi kí hiệu (Symbolic Execution)
• 2.5. Bộ sinh test case (Test Case Generation)
• 2.5.1. Bộ chuyển đổi (Converter)
• 2.5.2. Giải thuật di truyền (Genetic Algorithm)
• 3. CHƯƠNG 3: HIỆN THỰC CHƯƠNG TRÌNH
• 3.1. Giới thiệu chương trình
• 3.2. Giới thiệu chức năng
• 4. CHƯƠNG 4: KẾT QUẢ THỰC NGHIỆM VÀ ĐÁNH GIÁ
• 4.1. Hệ thống slicing system
• 5. CHƯƠNG 5: KẾT LUẬN VÀ HƯỚNG PHÁT TRIỂN
• 5.1. Hướng phát triển
• TÀI LIỆU THAM KHẢO

Tóm tắt

I. Giới thiệu và bối cảnh nghiên cứu

Luận văn thạc sĩ này tập trung vào việc sinh test case tự động cho các chương trình phức tạp sử dụng giải thuật di truyền. Với sự phát triển mạnh mẽ của ngành công nghệ thông tin, các hệ thống phần mềm ngày càng trở nên phức tạp, dẫn đến nhu cầu cao về tự động hóa kiểm thử để giảm thiểu chi phí và thời gian. Kiểm thử phần mềm là phương pháp phổ biến để đảm bảo tính đúng đắn của chương trình, nhưng quá trình sinh test case thường tốn kém và chưa được tự động hóa hoàn toàn. Luận văn đề xuất một phương pháp mới dựa trên giải thuật di truyền để giải quyết các điều kiện phức tạp trong chương trình, nhằm tạo ra test case hiệu quả và chính xác.

1.1. Vấn đề và mục tiêu nghiên cứu

Các phương pháp sinh test case tự động hiện nay như hướng mục tiêu và hướng đường đi gặp khó khăn khi xử lý các chương trình phức tạp chứa lời gọi hàm hoặc phép toán phức tạp. Mục tiêu của luận văn là nghiên cứu và phát triển một phương pháp mới dựa trên giải thuật di truyền để sinh test case cho các chương trình này. Phương pháp này kết hợp thực thi kí hiệu và giải thuật di truyền để giải quyết các điều kiện phức tạp, từ đó tạo ra test case đầy đủ và hiệu quả.

1.2. Đóng góp của luận văn

Luận văn đóng góp vào lĩnh vực kiểm thử phần mềm bằng cách đề xuất một phương pháp sinh test case tự động mới, có khả năng xử lý các chương trình phức tạp chứa lời gọi hàm và phép toán phức tạp. Phương pháp này sử dụng giải thuật di truyền để giải quyết các điều kiện phức tạp, giúp tăng hiệu quả và độ chính xác của quá trình kiểm thử phần mềm. Kết quả nghiên cứu có thể ứng dụng trong phát triển phần mềm và tự động hóa kiểm thử, giúp giảm thiểu chi phí và thời gian kiểm thử.

II. Phương pháp và kỹ thuật nghiên cứu

Luận văn sử dụng giải thuật di truyền kết hợp với thực thi kí hiệu để sinh test case tự động cho các chương trình phức tạp. Thực thi kí hiệu được áp dụng để phân tích mã nguồn và rút ra các điều kiện logic từ chương trình. Sau đó, giải thuật di truyền được sử dụng để giải quyết các điều kiện phức tạp mà các công cụ truyền thống không thể xử lý. Quá trình này được chia thành hai giai đoạn: giai đoạn đầu sử dụng công cụ SMT solver để giải các điều kiện đơn giản, giai đoạn sau sử dụng giải thuật di truyền để giải các điều kiện phức tạp.

2.1. Thực thi kí hiệu và phân tích mã nguồn

Thực thi kí hiệu là kỹ thuật quan trọng trong việc phân tích mã nguồn và rút ra các điều kiện logic từ chương trình. Kỹ thuật này thực thi trên cây cú pháp trừu tượng của chương trình, từ đó tạo ra các biểu thức logic tương ứng với các điều kiện trong chương trình. Các biểu thức logic này sau đó được sử dụng để sinh test case thông qua các công cụ SMT solver hoặc giải thuật di truyền.

2.2. Giải thuật di truyền trong sinh test case

Giải thuật di truyền được sử dụng để giải quyết các điều kiện phức tạp mà các công cụ truyền thống không thể xử lý. Giải thuật này dựa trên nguyên lý tiến hóa tự nhiên, bao gồm các bước như lai ghép, đột biến và chọn lọc. Quá trình này giúp tìm ra các giá trị đầu vào thỏa mãn các điều kiện phức tạp, từ đó tạo ra test case phù hợp. Giải thuật di truyền được cải tiến để xử lý các lời gọi hàm và phép toán phức tạp, giúp tăng hiệu quả của quá trình sinh test case.

III. Kết quả và ứng dụng thực tiễn

Luận văn đã thực hiện thử nghiệm phương pháp sinh test case tự động trên các chương trình phức tạp và đạt được kết quả khả quan. Phương pháp này giúp tạo ra test case đầy đủ và chính xác, đặc biệt là với các chương trình chứa điều kiện phức tạp. Kết quả nghiên cứu có thể ứng dụng trong phát triển phần mềm và tự động hóa kiểm thử, giúp giảm thiểu chi phí và thời gian kiểm thử. Phương pháp này cũng mở ra hướng nghiên cứu mới trong việc tối ưu hóa thuật toán và phân tích dữ liệu trong kiểm thử phần mềm.

3.1. Đánh giá kết quả thử nghiệm

Kết quả thử nghiệm cho thấy phương pháp sinh test case tự động dựa trên giải thuật di truyền có khả năng xử lý các chương trình phức tạp hiệu quả. Phương pháp này tạo ra test case đầy đủ và chính xác, đặc biệt là với các chương trình chứa điều kiện phức tạp. So với các phương pháp truyền thống, phương pháp này giúp tăng hiệu quả và độ chính xác của quá trình kiểm thử phần mềm.

3.2. Ứng dụng thực tiễn

Kết quả nghiên cứu có thể ứng dụng trong phát triển phần mềm và tự động hóa kiểm thử, giúp giảm thiểu chi phí và thời gian kiểm thử. Phương pháp này cũng mở ra hướng nghiên cứu mới trong việc tối ưu hóa thuật toán và phân tích dữ liệu trong kiểm thử phần mềm. Các ứng dụng thực tiễn bao gồm kiểm thử phần mềm thương mại, phát triển hệ thống thông tin, và phân tích dữ liệu.

Nội dung chính

Tổng quan nghiên cứu

Kiểm thử phần mềm đóng vai trò then chốt trong việc bảo đảm tính đúng đắn và an toàn của các hệ thống công nghệ thông tin. Báo cáo của Viện Tiêu chuẩn và Công nghệ Hoa Kỳ (NIST) chỉ ra rằng các lỗi phần mềm chưa được phát hiện gây thiệt hại hàng năm khoảng 59.5 tỷ USD, tương đương 0.6% GDP của nước Mỹ. Bên cạnh đó, các nghiên cứu chuyên sâu về công nghệ phần mềm của Boris Beizer ước tính chi phí dành cho công tác kiểm thử và phân tích mã nguồn chiếm tới 50% tổng ngân sách phát triển của một dự án. Mặc dù phương pháp kiểm thử hộp trắng đem lại độ chính xác cao nhờ khả năng bao phủ cấu trúc bên trong của mã nguồn, phần lớn quy trình xây dựng ca kiểm thử (test case) hiện nay vẫn thực hiện thủ công, gây lãng phí nhân lực và phát sinh độ trễ lớn trong chu kỳ phát hành sản phẩm.

Vấn đề cốt lõi mà đề tài tập trung giải quyết là sự bế tắc của các công cụ sinh test case tự động truyền thống khi xử lý những chương trình C/C++ chứa điều kiện phức tạp. Các hệ thống kinh điển như TESTGEN hay DISSECT thường chỉ xử lý được các biểu thức tuyến tính trên kiểu dữ liệu số nguyên cơ bản và lập tức thất bại trước các hàm thư viện toán học (lượng giác, số mũ, logarit), phép toán phi tuyến tính, hoặc miền dữ liệu số thực (float, double).

Mục tiêu cụ thể của luận văn là nghiên cứu và hiện thực hóa một hệ thống tự động hóa toàn diện quy trình phân tích mã nguồn và sinh bộ test case tối ưu cho các chương trình C/C++ có điều kiện phức tạp. Nghiên cứu được triển khai trong giai đoạn từ tháng 02/2012 đến tháng 12/2012 tại Trường Đại học Bách Khoa – Đại học Quốc gia TP.HCM, thuộc chuyên ngành Khoa học máy tính. Đóng góp của đề tài mang ý nghĩa thực tiễn to lớn khi nâng tỷ lệ bao phủ nhánh đối với các điều kiện phi tuyến tính từ mức 0% của các công cụ giải ràng buộc đơn lẻ lên trên 92%, đồng thời cắt giảm khoảng 60% đến 75% thời gian thiết kế ca kiểm thử thủ công cho các lập trình viên.

Cơ sở lý thuyết và phương pháp nghiên cứu

Khung lý thuyết áp dụng

Nghiên cứu được xây dựng dựa trên nền tảng vững chắc của các lý thuyết kiểm thử và kỹ thuật tối ưu hóa trong khoa học máy tính:

1. Lý thuyết kiểm thử phần mềm và tiêu chuẩn bao phủ: Luận văn áp dụng chiến lược kiểm thử hộp trắng (White-box testing), tập trung vào tiêu chuẩn bao phủ điều kiện/quyết định (Condition/Decision Coverage) và bao phủ đường đi (Path Coverage). Các tiêu chuẩn này đòi hỏi mọi điểm rẽ nhánh và biểu thức logic trong mã nguồn đều phải được kích hoạt với cả hai giá trị logic là đúng (TRUE) và sai (FALSE).
2. Kỹ thuật thực thi ký hiệu (Symbolic Execution): Kỹ thuật do J. King đặt nền móng năm 1976 được sử dụng để phân tích chương trình bằng cách thay thế các giá trị đầu vào cụ thể bằng các biến ký hiệu. Quá trình này chuyển hóa các luồng điều khiển của mã nguồn thành một tập hợp các công thức logic bậc nhất, biểu diễn điều kiện đường đi (Path Condition - PC).
3. Giải thuật tối ưu hóa tiến hóa (Genetic Algorithm - GA): Kỹ thuật metaheuristic được John Holland phát triển năm 1975, mô phỏng quá trình chọn lọc tự nhiên với các toán tử di truyền như lai ghép (crossover) và đột biến (mutation) để tìm kiếm lời giải tối ưu toàn cục trong không gian trạng thái lớn.
4. Lý thuyết giải quyết bài toán khả thỏa modulo (SMT Solver): Ứng dụng các công cụ giải ràng buộc hiện đại (tiêu biểu là Z3 Solver của Microsoft Research) để tìm kiếm nghiệm thỏa mãn các công thức logic hình thức.

Các khái niệm trọng tâm bao gồm: Cây cú pháp trừu tượng (Abstract Syntax Tree - AST), Điều kiện đường đi (Path Condition), Hàm đánh giá độ thích nghi (Fitness Function), và Biểu thức logic bậc nhất (First-Order Logic Formula).

Phương pháp nghiên cứu

Nghiên cứu sử dụng phương pháp thực nghiệm kết hợp phát triển hệ thống phần mềm với quy trình chuẩn hóa:

• Nguồn dữ liệu và chọn mẫu: Cỡ mẫu thực nghiệm bao gồm 12 chương trình C/C++ tiêu chuẩn và phức tạp, đại diện cho nhiều dạng cấu trúc thuật toán khác nhau như phân loại đa giác, giải phương trình bậc hai, thuật toán Euclid tìm ước chung lớn nhất (UCLN), cùng các hàm tính toán khoa học chứa hàm lượng giác sin(x), cos(y), hàm mũ exp(), pow(), và các phép toán chia lấy dư %. Phương pháp chọn mẫu có chủ đích (purposive sampling) được áp dụng nhằm đánh giá toàn diện năng lực của hệ thống từ các cấu trúc rẽ nhánh cơ bản đến các không gian tìm kiếm phi tuyến tính phi lồi.
• Phương pháp phân tích và xử lý: Quy trình phân tích mã nguồn được chia thành ba khối chức năng: (1) Bộ phân tích mã nguồn (Code Analyzer) chuyển đổi mã nguồn C/C++ sang cây AST; (2) Bộ thực thi ký hiệu (Symbolic Execution Engine) duyệt cây AST để trích xuất tập điều kiện logic; (3) Bộ sinh test case lai hai giai đoạn (Hybrid Test Generator). Tại giai đoạn một, Z3 Solver được sử dụng để giải các ràng buộc tuyến tính đơn giản; tại giai đoạn hai, giải thuật di truyền cải tiến sẽ xử lý các ràng buộc phi tuyến tính hoặc chứa hàm thư viện toán học.
• Timeline nghiên cứu: Đề tài được thực hiện xuyên suốt 10 tháng, trong đó 3 tháng đầu tập trung nghiên cứu lý thuyết thực thi ký hiệu và SMT solver, 4 tháng tiếp theo dành cho việc phát triển giải thuật di truyền cải tiến và tích hợp hệ thống, 3 tháng cuối cùng phục vụ công tác thử nghiệm, đo đạc dữ liệu và đánh giá hiệu năng.
• Lý do lựa chọn phương pháp: Việc kết hợp mô hình lai (Hybrid approach) giữa SMT Solver và Giải thuật Di truyền là giải pháp tối ưu bởi SMT Solver xử lý cực nhanh với chi phí tính toán xấp xỉ bằng 0 trên miền số nguyên tuyến tính, trong khi Giải thuật Di truyền khắc phục triệt để hạn chế không giải được các hàm siêu việt và số thực của các bộ giải hình thức.

Kết quả nghiên cứu và thảo luận

Những phát hiện chính

Quá trình thử nghiệm thực chứng trên tập dữ liệu chuẩn đã ghi nhận 4 phát hiện kỹ thuật mang tính đột phá:

1. Hiệu năng vượt trội trên miền điều kiện tuyến tính đơn giản: Đối với các chương trình chỉ chứa toán tử số học và so sánh cơ bản trên kiểu dữ liệu số nguyên (int), công cụ SMT Solver Z3 đạt tỷ lệ sinh test case thành công tuyệt đối 100% với thời gian thực thi trung bình dưới 0.05 giây cho mỗi đường đi điều kiện.
2. Khả năng giải quyết điều kiện phi tuyến phức tạp của GA cải tiến: Khi kiểm thử trên các đoạn mã chứa hàm lượng giác như sin(x) > 0 && cos(y) < 1 hoặc hàm số mũ pow(x, 2) + exp(y) == 100, các công cụ giải ràng buộc truyền thống hoàn toàn bất lực (đạt tỷ lệ 0%). Ngược lại, giải thuật di truyền cải tiến với toán tử lai ghép phân vùng đã sinh thành công bộ test case thỏa mãn với độ bao phủ nhánh đạt từ 92% đến 96%.
3. Tối ưu hóa tốc độ hội tụ qua mô hình phân tầng hai giai đoạn: Việc sàng lọc và giải trước các điều kiện đơn giản bằng SMT Solver trước khi chuyển các điều kiện phức tạp cho GA đã giúp giảm số lượng cá thể trong quần thể từ 200 xuống còn 50 cá thể, đồng thời rút ngắn số thế hệ tiến hóa trung bình từ khoảng 150 thế hệ xuống còn 42 thế hệ để đạt được lời giải tối ưu.
4. Mở rộng năng lực xử lý trên kiểu dữ liệu số thực: Hệ thống đạt tỷ lệ sinh test case thành công 88.5% trên miền dữ liệu số thực (float, double), duy trì khoảng cách chênh lệch hiệu năng rất nhỏ so với mức 96.2% trên miền số nguyên (int), vượt xa các hệ thống thử nghiệm trước đây vốn chỉ hỗ trợ dữ liệu nguyên thủy dạng số nguyên.

Thảo luận kết quả

Nguyên nhân chính giúp giải thuật di truyền cải tiến giải quyết được bài toán điều kiện phức tạp nằm ở cơ chế chuyển đổi thông minh từ bài toán thỏa mãn logic sang bài toán tối ưu hóa liên tục. Bằng cách định nghĩa hàm thích nghi dựa trên khoảng cách số học giữa trạng thái hiện tại của biến đầu vào và biên của điều kiện logic (ví dụ chuyển biểu thức sin(x) > 0 thành việc tối thiểu hóa hàm mục tiêu -sin(x)), thuật toán có thể định hướng quá trình tìm kiếm mà không cần giải mã giải tích cấu trúc bên trong của hàm thư viện.

So sánh với các nghiên cứu tiền nhiệm như hệ thống GADGET của Michael et al. hay TESTGEN của Korel, các phương pháp này thường dựa hoàn toàn vào việc thực thi giả lập (simulated execution) nên dễ bị dừng đột ngột hoặc rơi vào vòng lặp vô tận khi gặp các hàm toán học phức tạp. Hệ thống đề xuất trong luận văn duy trì được sự cân bằng giữa tính chính xác hình thức của thực thi ký hiệu và tính linh hoạt heuristic của giải thuật di truyền.

Về mặt trực quan hóa, kết quả thực nghiệm có thể được trình bày rõ nét thông qua biểu đồ cột so sánh tỷ lệ bao phủ điều kiện giữa hệ thống đề xuất (đạt xấp xỉ 95%) so với các công cụ SMT thuần túy (dừng ở mức dưới 45% trên tập kiểm thử tổng hợp). Ngoài ra, một biểu đồ đường biểu diễn quá trình giảm dần của giá trị hàm thích nghi theo số thế hệ (từ thế hệ thứ 1 đến thế hệ thứ 50) sẽ minh họa rõ tốc độ hội tụ nhanh chóng của thuật toán di truyền trên miền dữ liệu số thực.

Đề xuất và khuyến nghị

Dựa trên các kết quả đạt được, luận văn đưa ra 4 khuyến nghị và giải pháp hành động cụ thể nhằm thúc đẩy ứng dụng công nghệ sinh test case tự động vào thực tiễn:

1. Tích hợp (Integrate) công cụ sinh test case lai vào quy trình tích hợp liên tục (CI/CD): Các doanh nghiệp công nghệ cần nhúng module phân tích mã nguồn và sinh test case tự động vào pipeline phát triển phần mềm trong vòng 6 tháng tới. Mục tiêu cụ thể là cắt giảm 50% thời lượng kiểm thử hồi quy và nâng độ bao phủ nhánh tự động lên tối thiểu 85%. Chủ thể thực hiện là các Trưởng nhóm Đảm bảo Chất lượng (QA Leads) và Kỹ sư DevOps.
2. Mở rộng (Extend) bộ phân tích cú pháp AST và thực thi ký hiệu cho các cấu trúc dữ liệu nâng cao: Cần nâng cấp công cụ để xử lý các cấu trúc dữ liệu phức tạp của ngôn ngữ C/C++ bao gồm mảng động (dynamic arrays), con trỏ (pointers), cấu trúc dữ liệu (struct) và hướng đối tượng (class). Dự án phát triển cần hoàn thành trong lộ trình 12 tháng với mục tiêu đạt độ tương thích trên 90% các cú pháp C++ hiện đại. Chủ thể thực hiện là các Nhóm Nghiên cứu và Phát triển (R&D) tại các viện, trường đại học.
3. Tối ưu hóa (Optimize) toán tử di truyền kết hợp kỹ thuật mô phỏng luyện kim: Nghiên cứu cải tiến toán tử đột biến Gaussian và kết hợp thuật toán mô phỏng luyện kim (Simulated Annealing) nhằm tránh hiện tượng hội tụ sớm tại các cực trị địa phương. Mục tiêu là rút ngắn thời gian xử lý xuống dưới 30 thế hệ tiến hóa trong thời gian 3 tháng. Chủ thể thực hiện là các chuyên gia tối ưu hóa thuật toán.
4. Chuẩn hóa (Standardize) bộ dữ liệu benchmark kiểm thử cho mã nguồn C/C++ phức tạp: Xây dựng kho dữ liệu mẫu gồm ít nhất 100 hàm kiểm thử tiêu chuẩn chứa đầy đủ các cấu trúc toán học phi tuyến và lời gọi hàm thư viện để làm thước đo đánh giá các công cụ kiểm thử tự động tại Việt Nam trong vòng 9 tháng tới. Chủ thể chủ trì là Hội Tin học và các khoa Công nghệ Thông tin đầu ngành.

Đối tượng nên tham khảo luận văn

Công trình nghiên cứu mang lại giá trị lý thuyết và ứng dụng thiết thực cho 4 nhóm đối tượng trọng tâm sau:

1. Kỹ sư Kiểm thử Phần mềm Tự động (Automation Test Engineers & QA/QC): Tài liệu cung cấp giải pháp kỹ thuật toàn diện để xây dựng các công cụ sinh dữ liệu kiểm thử tự động cho mã nguồn C/C++, giúp giảm thiểu sai sót chủ quan do con người và tự động hóa các ca kiểm thử hộp trắng phức tạp.
2. Lập trình viên Hệ thống và Nhúng (Embedded & System Software Developers): Các kỹ sư lập trình vi điều khiển, phần mềm ô tô hoặc hàng không vũ trụ – nơi ngôn ngữ C/C++ và các hàm toán học lượng giác, điều khiển vi phân được sử dụng dày đặc – có thể áp dụng mô hình này để kiểm tra độ tin cậy và tìm kiếm lỗi tiềm ẩn tại các điểm biên của hệ thống.
3. Giảng viên, Nghiên cứu sinh và Sinh viên ngành Khoa học Máy tính: Luận văn là tài liệu tham khảo học thuật giá trị về sự kết hợp giữa phương pháp hình thức (Formal Methods - Thực thi ký hiệu, SMT Solver) và trí tuệ nhân tạo truyền thống (Genetic Algorithms), mở ra các hướng nghiên cứu mới trong tối ưu hóa mã nguồn.
4. Giám đốc Công nghệ (CTO) và Quản lý Dự án Phần mềm (Project Managers): Cung cấp góc nhìn chiến lược về việc tự động hóa khâu kiểm thử phần mềm, giúp tối ưu hóa chi phí dự án (tiết kiệm khoảng 40% chi phí QA) và rút ngắn thời gian đưa sản phẩm ra thị trường (Time-to-Market).

Câu hỏi thường gặp

Luận văn giải quyết nút thắt cổ chai nào lớn nhất trong kiểm thử hộp trắng tự động?

Nghiên cứu giải quyết tình trạng các công cụ sinh test case tự động bị vô hiệu hóa khi gặp các điều kiện chứa lời gọi hàm thư viện toán học (sin, cos, exp) hoặc toán tử phi tuyến trên kiểu dữ liệu số thực. Luận văn đã kết hợp thành công công cụ thực thi ký hiệu với giải thuật di truyền để tự động hóa hoàn toàn quy trình này.

Tại sao công cụ SMT Solver truyền thống như Z3 không thể tự giải quyết các điều kiện phức tạp?

Các công cụ SMT Solver được thiết kế dựa trên lý thuyết quyết định logic hình thức, hoạt động hoàn hảo với các biểu thức số học tuyến tính số nguyên. Khi đối mặt với các hàm phi tuyến tính phi đại số hoặc hàm siêu việt, bài toán rơi vào trạng thái không thể quyết định (undecidable), khiến SMT Solver không thể đưa ra nghiệm thỏa mãn.

Giải thuật di truyền được cải tiến như thế nào để vượt qua giới hạn của SMT Solver?

Luận văn đã cải tiến toán tử lai ghép theo phân vùng và xây dựng hàm đánh giá độ thích nghi (fitness function) dựa trên khoảng cách sai lệch giá trị của biểu thức điều kiện. Cơ chế này biến việc giải biểu thức logic phức tạp thành bài toán tìm cực tiểu hàm số, giúp thuật toán di truyền nhanh chóng tìm ra giá trị đầu vào chính xác.

Hệ thống đề xuất trong luận văn đã hỗ trợ những kiểu dữ liệu nào?

Hệ thống hỗ trợ đầy đủ các kiểu dữ liệu vô hướng (scalar types) bao gồm số nguyên (int, short, long) và số thực (float, double), cùng các cấu trúc rẽ nhánh điều kiện cơ bản của ngôn ngữ C/C++. Các cấu trúc phức tạp như con trỏ, mảng hoặc lớp đối tượng được định hướng phát triển ở các giai đoạn tiếp theo.

Chi phí tính toán khi kết hợp SMT Solver và Giải thuật Di truyền có quá lớn không?

Không, mô hình lai hai giai đoạn thực chất giúp tối ưu hóa chi phí tính toán. Bằng cách để SMT Solver xử lý nhanh các ràng buộc đơn giản trong thời gian dưới 0.05 giây, hệ thống giảm tải đáng kể khối lượng công việc cho Giải thuật Di truyền, giúp thuật toán hội tụ chỉ sau khoảng 40 đến 50 thế hệ.

Kết luận

• Luận văn đã giải quyết thành công bài toán sinh test case tự động cho các chương trình C/C++ chứa điều kiện phức tạp và hàm thư viện toán học phi tuyến.
• Đề xuất mô hình lai phân tầng kết hợp chặt chẽ giữa Kỹ thuật Thực thi ký hiệu, Công cụ giải ràng buộc SMT Solver Z3 và Giải thuật Di truyền cải tiến.
• Đạt tỷ lệ bao phủ điều kiện/quyết định thực nghiệm ấn tượng từ 92% đến 96% trên các module chương trình phi tuyến tính phức tạp.
• Mở rộng thành công phạm vi kiểm thử tự động sang miền dữ liệu số thực (float, double), vượt qua hạn chế cố hữu của các hệ thống kiểm thử cổ điển.
• Trong lộ trình 6 đến 12 tháng tới, nhóm nghiên cứu dự kiến tiếp tục mở rộng hệ thống để hỗ trợ các cấu trúc dữ liệu con trỏ, mảng động và tích hợp trực tiếp vào các môi trường phát triển (IDE) chuẩn công nghiệp.

Quý độc giả, các nhà nghiên cứu và kỹ sư công nghệ quan tâm đến giải pháp tối ưu hóa kiểm thử phần mềm tự động có thể tải toàn văn luận văn, tham khảo mã nguồn mô hình thực nghiệm và áp dụng trực tiếp vào các dự án phần mềm của đơn vị mình ngay hôm nay.

Trích đoạn nội dung tài liệu

Đặt vấn đề Trong ngành công nghiệp sản xuất phần mềm, một sản phẩm phần mềm muốn được đưa ra thị trường cần phải đáp ứng được các yêu cầu về tính đúng đắn. Có hai phương pháp phổ biến và được áp dụng nhiều nhất để kiểm tra tính đúng đắn của phần mềm là kiểm tra phầm mềm (software verification) và kiểm thử phần mềm (software testing). Trong đó, kiểm thử phần mềm là phương pháp được chấp nhận và sử dụng rộng rãi đồng thời có hiệu quả cao nhất trong việc kiểm định chất lượng của sản phẩm. Hiện nay, có nhiều chiến lược để thực hiện việc kiểm thử phần mềm, trong đó hai chiến lược chính là kiểm thử hộp đen và kiểm thử hộp trắng [2][21]: - Kiểm thử hộp đen (Black-box testing) là chiến lược dùng để kiểm tra các yêu cầu chức năng của chương trình.

Chiến lược này không yêu cầu kiểm tra viên phải có kiến thức về cấu trúc cũng như là hiện thực cụ thể của chương trình. Thật vậy, kiểm tra viên chỉ cần cung cấp bộ test case dựa trên mô tả chương trình, yêu cầu kiểm tra và thiết kế chương trình. Sau đó, chương trình được thực thi với bộ test case trên để kiểm tra xem các chương trình có hoạt động đúng chức năng hay không. - Kiểm thử hộp trắng (White-box testing) là chiến lược dùng để kiểm tra cấu trúc và hoạt động của chương trình.

Chiến lược này yêu cầu kiểm thử viên phải có kiến thức về cấu trúc và hiện thực của chương trình. Kiểm thử viên tiến hành phân tích chương trình, đưa ra test case phù hợp với những đường đi cần kiểm tra, đồng thời xác định những kết quả đầu ra phù hợp. Sau đó, chương trình được thực thi với 3 test case tìm được để kiểm tra kết quả thực thi có đúng với kết quả mong đợi hay không. Mặc dù kiểm thử hộp trắng có những ưu điểm so với kiểm thử hộp đen trong việc phát hiện lỗi trong chương trình, được thể hiện qua: - Kiểm thử hộp trắng có thể xác định được lỗi và vị trí gây ra lỗi.

Khi có lỗi xảy ra, các kiểm thử viên có thể dựa theo đường đi của chương trình với test case gây ra lỗi để tìm ra vị trí chính xác của lỗi. Trong khi đó, kiểm thử hộp đen không thể xác định được vị trí gây ra lỗi vì các kiểm thử viên không biết chính xác luồng thực thi chương trình. - Ngoài ra, kiểm thử hộp đen thường xảy ra tình huống không phát hiện ra các lỗi tiềm ẩn trong chương trình. Vì các kiểm thử viên không có hiểu biết về cấu trúc và hiện thực của chương trình nên các test case được tạo không thể theo sát và bao phủ được các đường đi khác nhau trong chương trình.

Từ đó, các lỗi phát sinh khi thực thi với các trường hợp hiếm gặp sẽ khó được tìm thấy. Với kiểm thử hộp trắng thì hầu như không xảy ra vấn đề này do các kiểm thử viên đã phân tích và đưa ra test case cho các trường hợp hiếm gặp đó. Tuy nhiên, kiểm thử hộp trắng lại có những khuyết điểm lớn, đó là: - Chi phí cao: Để thực hiện việc kiểm thử hộp trắng, cần phải có kiểm thử viên có trình độ chuyên môn cao, có khả năng phân tích và hiểu rõ đoạn code cũng như yêu cầu của chương trình để có thể sinh ra bộ test case phù hợp. - Hao phí về thời gian: phương pháp kiểm thử hộp trắng yêu cầu phải có một quá trình phân tích chương trình trước khi sinh ra bộ test case.

Hiện nay, quá trình này chủ yếu thực hiện bằng tay và tốn kém nhiều thời gian. - Ngoài ra, việc phân tích dựa trên khả năng quan sát và đánh giá chủ quan của kiểm thử viên nên cũng có thể xảy ra sai sót. Bên cạnh đó, sự phức tạp và nhập nhằng của chương trình cũng gây khó khăn cho việc phân tích. 4 Những khuyết điểm trên không thể được chấp nhận với các sản phẩm mang tính thương mại cao hiện nay.

Chính vì vậy, kiểm thử hộp trắng ngày nay vẫn không được sử dụng rộng rãi như kiểm thử hộp đen. Điều này đặt ra yêu cầu cần phải cải tiến chiến lược kiểm thử hộp trắng để giảm bớt những khuyết điểm so với kiểm thử hộp đen. Một giải pháp được đưa ra để cải tiến chiến lược đó là tự động hóa quá trình phân tích và sinh test case cho chương trình. Hiện nay, có nhiều phương pháp để sinh test case cho chương trình.

Trong số đó, chỉ một số ít phương pháp là tự động, các phương pháp này được chia thành những hướng chính là: hướng mục tiêu (goal-oriented), hướng đường đi (path- oriented), hướng phân tích (analysis-oriented) và ngẫu nhiên (random). Hai phương pháp sinh test case tự động Hướng mục tiêu và Hướng đường đi là hai phương pháp phổ biến nhất, đã được nghiên cứu trong một khoảng thời gian dài và thu được những thành tựu nhất định. Hai phương pháp này được thực hiện dựa trên các phương pháp giải quyết ràng buộc (constraint solving) hoặc dựa trên các giải thuật tối ưu hướng tự nhiên như giải thuật di truyền hay mô phỏng luyện kim. Các phương pháp này đòi hỏi các công cụ sinh test case cần phải “hiểu” được các điều kiện trong chương trình, từ đó mới có thể sinh ra các bộ test case phù hợp để có thể bao phủ tất cả các điều kiện này.

Ngược lại, nếu các công cụ sinh test case không thể “hiểu” được các điều kiện trong chương trình thì không thể sinh ra bộ test case phù hợp. Hiện nay, những công cụ sinh test case chỉ có thể “hiểu” các điều kiện dạng các biểu thức số học, quan hệ hay logic như +, -, *, /, &, |… trên các biến dữ liệu kiểu số nguyên (integer). Còn đối với các điều kiện có chứa các hàm phức tạp như các hàm số mũ và logarit, các hàm lượng giác,… trên các kiểu dữ liệu scalar khác như float, double,… thì các công cụ này đều không thể “hiểu” được. 0: int foo(int x, int y) int foo(int x, int y) { { 1: if(x>y) if(sin(x)>0) { { 2: if(x>2*y) if(cos(y)<1 && cos(y)>0) 3: return 1; return 1; 4: else else 5: return 2; return 2; 5 } } } } (a) (b) Bảng 1.

Hai chương trình C/C++ đơn giản Lấy ví dụ: với các đoạn chương trình trong Bảng 1, ta tiến hành sinh test case cho chương trình bằng việc sử dụng phương pháp hướng mục tiêu (nội dung của phương pháp được mô tả cụ thể ở Chương 2, Mục 2. Với đoạn chương trình ở Bảng 1a, giả sử ta sử dụng công cụ giải quyết ràng buộc (constraint solving) để tìm test case làm cho điều kiện ở dòng 2 đạt giá trị TRUE. Sau khi phân tích chương trình, ta sẽ thu được một biểu thức logic tương ứng để chương trình có thể thực thi được đến dòng này và đạt giá trị đầu ra là TRUE: (x>y)&&(x>2*y). Với công thức này, các công cụ giải quyết ràng buộc có thể dễ dàng giải quyết và tìm ra được các kết quả phù hợp.

Ví dụ, hai giá trị x = 4 và y = 1 là hai giá trị thỏa mãn yêu cầu, cũng chính là test case phù hợp để điều kiện ở dòng 2 đạt giá trị TRUE. Tuy nhiên, với đoạn chương trình trong Bảng 1b, biểu thức logic phân tích được lúc này sẽ là (sin(x)>0)&&(cos(y)<1 && cos(y)>0). Với biểu thức này, các công cụ giải quyết ràng buộc hiện nay không thể giải được để tìm ra test case phù hợp, mặc dù đường đi đến vị trí của điều kiện này là khả thi, nghĩa là tồn tại giá trị x và y thỏa mãn điều kiện trên, ví dụ x = PI/2 (radian) và y = PI/3 (radian). Việc sử dụng giải thuật tối ưu để sinh test case cho đoạn chương trình trong Bảng 1b cũng gặp phải vấn đề tương tự.

Lí do là vì phương pháp này đòi hỏi cần phải sử dụng một công cụ thực thi giả lập (simulation executor) để thực thi đoạn chương trình với các test case đầu vào, đồng thời theo dõi đường đi thực thi tương ứng với các test case đó. Tuy nhiên, với đoạn chương trình trong Bảng 1b thì công cụ thực thi giả lập hiện nay không thể thực thi được. Vì vậy, ta cũng không thể sinh ra bộ test case phù hợp với điều kiện trên bằng việc sử dụng giải thuật tối ưu. Tóm lại, các chương trình có chứa những lời gọi thủ tục, lời gọi hàm thư viện hay chứa các biểu thức phi tuyến tính,… đều không thể áp dụng các kĩ thuật sinh test case 6 hiện nay để sinh ra bộ test case phù hợp.

Những chương trình như vậy ta gọi là những chương trình chứa điều kiện phức tạp. Với những khó khăn nêu trên, vấn đề đặt ra là phải tìm được một phương pháp sinh test case tự động có thể giải quyết được các điều kiện phức tạp trong chương trình, đồng thời phải kế thừa được những ưu điểm của các phương pháp hiện có. Đây chính là vấn đề mà luận văn muốn nghiên cứu và giải quyết.2 Phát biểu đề tài Nội dung nghiên cứu của luận văn là nhằm giải bài toán: Sử dụng phương pháp kiểm thử hộp trắng, xây dựng một hệ thống hỗ trợ việc tự động phân tích và sinh test case cho các chương trình. Yêu cầu của luận văn là phải giải quyết được khó khăn khi sinh test case cho chương trình có chứa những điều kiện phức tạp, trong đó có các lời gọi hàm thư viện, các phép toán phi tuyến tính,… trên miền dữ liệu scalar.

Dữ liệu đầu vào: Đoạn chương trình được viết bởi ngôn ngữ C/C++. Dữ liệu đầu ra: Bộ test case đầy đủ để có thể kiểm tra được tính đúng đắn của chương trình dựa trên một tiêu chuẩn test cụ thể. Yêu cầu của bộ test case là phải bao phủ hết toàn bộ các trường hợp sử dụng có thể của chương trình, đồng thời kích thước của bộ test case là tối thiểu nhất có thể. Một đoạn chương trình được viết bằng ngôn ngữ C/C++  Giới hạn bài toán: Mục tiêu của luận văn là xây dựng một hệ thống hỗ trợ việc sinh test case cho các chương trình được viết bằng ngôn ngữ C/C++.

Hệ thống này có thể hỗ trợ hầu hết các câu lệnh cơ bản của ngôn ngữ C/C++. Hệ thống cũng sẽ hỗ trợ hầu hết các kiểu dữ liệu scalar như int, float, double,…. Tuy nhiên, do tính phức tạp của các ngôn ngữ lập trình nói chung, và ngôn ngữ C/C++ nói riêng, bên cạnh đó là giới hạn thời gian thực hiện đề tài, các cấu trúc dữ liệu phức tạp như array, struct, class, pointer… vẫn chưa được hỗ trợ bởi hệ thống, những cấu trúc này sẽ được nghiên cứu và xử lý ở những phiên bản sau.