Luận Văn Thạc Sĩ Về Phương Pháp Sinh Dữ Liệu Kiểm Thử Tự Động Trong Ứng Dụng Java

Luận văn thạc sĩ nghiên cứu phương pháp sinh dữ liệu kiểm thử tự động cho các ứng dụng java, đánh giá hiện trạng, phân tích vấn đề, đề xuất biện pháp hoàn thiện trong lĩnh vực .

• Tác giả: Phan Thị Thu Hà
• Người hướng dẫn: TS. Phạm Ngọc Hùng
• Trường học: Đại học Quốc gia Hà Nội
• Chuyên ngành: Công nghệ thông tin
• Đề tài: Phương Pháp Sinh Dữ Liệu Kiểm Thử Tự Động Cho Ứng Dụng Java
• Loại tài liệu: luận văn thạc sĩ
• Năm xuất bản: 2015
• Địa điểm: Hà Nội

Mục lục chi tiết

• LỜI CAM ĐOAN
• 1. CHƯƠNG 1: GIỚI THIỆU
• 2. CHƯƠNG 2: CÁC KỸ THUẬT KIỂM THỬ DÒNG ĐIỀU KHIỂN
• 2.1. Tổng quan về kiểm thử hộp trắng
• 2.2. Kỹ thuật kiểm thử dòng điều khiển
• 2.3. Kiểm thử hộp trắng dòng điều khiển theo hướng động
• 2.4. Kiểm thử hộp trắng dòng điều khiển theo hướng tĩnh
• 2.5. Quy trình kiểm thử hộp trắng dòng điều khiển theo hướng tĩnh
• 2.6. Đồ thị dòng điều khiển
• 2.7. Các tiêu chí phủ kiểm thử
• 2.8. Đường kiểm thử
• 2.9. So sánh kĩ thuật kiểm thử hộp trắng dòng điều khiển theo hướng tĩnh và động
• 2.10. Tầm quan trọng của tự động hóa quy trình kiểm thử hộp trắng dòng điều khiển
• 3. CHƯƠNG 3: PHƯƠNG PHÁP KIỂM THỬ DÒNG ĐIỀU KHIỂN HƯỚNG TĨNH CHO CÁC HÀM JAVA
• 3.1. Xây dựng đồ thị dòng điều khiển từ mã nguồn
• 3.2. Xây dựng tập đường kiểm thử
• 3.3. Xây dựng tập đường đi độc lập
• 3.4. Xây dựng đường kiểm thử vòng lặp
• 3.5. Xây dựng hệ ràng buộc
• 3.6. Sinh tập dữ liệu kiểm thử dựa trên giải nghiệm hệ ràng buộc
• 3.7. Giải hệ sử dụng kỹ thuật sinh ngẫu nhiên
• 3.8. Giải hệ sử dụng SMT-Solver
• 4. CHƯƠNG 4: GIỚI THIỆU CÔNG CỤ
• 4.1. Kiến trúc công cụ
• 4.2. Nền tảng chương trình
• 4.3. Thư viện JDT
• 4.4. Bộ giải hệ Z3 Prover
• 4.5. Cài đặt công cụ
• 4.6. Đầu vào công cụ JavaUnitCFT
• 4.7. Đầu ra công cụ
• 5. CHƯƠNG 5: THỰC NGHIỆM
• 5.1. Sinh bộ dữ liệu kiểm thử cho hàm đầu vào chứa biến số nguyên
• 5.2. Sinh bộ dữ liệu kiểm thử cho hàm đầu vào chứa biến số thực
• 5.3. Sinh bộ dữ liệu kiểm thử cho hàm đầu vào chứa vòng lặp
• 6. CHƯƠNG 6: KẾT LUẬN
• TÀI LIỆU THAM KHẢO

Tóm tắt

I. Giới thiệu

Trong bối cảnh phát triển phần mềm hiện nay, kiểm thử tự động trở thành một phần không thể thiếu trong quy trình phát triển. Phương pháp sinh dữ liệu kiểm thử tự động cho ứng dụng Java được nghiên cứu nhằm giải quyết các vấn đề liên quan đến kiểm thử tự động. Việc áp dụng kỹ thuật kiểm thử hộp trắng giúp phát hiện lỗi tiềm ẩn trong mã nguồn, từ đó nâng cao chất lượng sản phẩm. Theo thống kê, kiểm thử có thể chiếm đến 40% - 60% tổng chi phí phát triển phần mềm. Do đó, việc tối ưu hóa quy trình kiểm thử là rất cần thiết. Luận văn này sẽ trình bày quy trình sinh dữ liệu kiểm thử tự động, từ việc phân tích mã nguồn đến việc sinh tập dữ liệu kiểm thử, nhằm đảm bảo độ bao phủ cao và độ tin cậy trong kiểm chứng tính đúng đắn của mã nguồn.

II. Các kỹ thuật kiểm thử dòng điều khiển

Chương này trình bày tổng quan về kiểm thử hộp trắng, đặc biệt là kiểm thử dòng điều khiển. Kỹ thuật này cho phép kiểm tra cấu trúc bên trong của chương trình, đảm bảo rằng tất cả các câu lệnh và điều kiện được thực hiện ít nhất một lần. Kiểm thử hộp trắng được chia thành hai kỹ thuật chính: kỹ thuật tĩnh và kỹ thuật động. Kỹ thuật tĩnh phân tích mã nguồn mà không thực thi chương trình, trong khi kỹ thuật động yêu cầu thực thi chương trình để kiểm tra. Việc áp dụng kỹ thuật kiểm thử hộp trắng giúp phát hiện lỗi sớm hơn và giảm thiểu chi phí sửa lỗi sau này. Tầm quan trọng của việc tự động hóa quy trình kiểm thử cũng được nhấn mạnh, giúp tiết kiệm thời gian và nguồn lực.

2.1. Kỹ thuật kiểm thử hộp trắng

Kỹ thuật kiểm thử hộp trắng cho phép kiểm tra cấu trúc bên trong của chương trình. Dữ liệu kiểm thử được sinh ra từ việc phân tích mã nguồn, giúp đảm bảo rằng tất cả các câu lệnh và điều kiện được thực hiện ít nhất một lần. Kỹ thuật này có thể phát hiện lỗi tiềm ẩn mà kiểm thử hộp đen không thể phát hiện. Việc áp dụng kỹ thuật này trong kiểm thử tự động giúp nâng cao chất lượng phần mềm và giảm thiểu rủi ro trong quá trình phát triển.

2.2. Kỹ thuật kiểm thử dòng điều khiển

Kỹ thuật kiểm thử dòng điều khiển tập trung vào việc kiểm tra các đường đi trong mã nguồn. Đồ thị dòng điều khiển được xây dựng từ mã nguồn, từ đó sinh ra các đường kiểm thử. Việc này giúp đảm bảo rằng tất cả các nhánh và vòng lặp trong mã nguồn đều được kiểm tra. Kỹ thuật này có thể được áp dụng để sinh dữ liệu kiểm thử cho các hàm Java, đảm bảo rằng các trường hợp kiểm thử được thực hiện đầy đủ và chính xác.

III. Phương pháp sinh dữ liệu kiểm thử tự động

Phương pháp sinh dữ liệu kiểm thử tự động cho ứng dụng Java được xây dựng dựa trên kỹ thuật kiểm thử hộp trắng dòng điều khiển. Quy trình bắt đầu bằng việc phân tích mã nguồn để sinh đồ thị dòng điều khiển. Từ đồ thị này, tập đường kiểm thử được xây dựng, bao gồm cả các đường kiểm thử chứa vòng lặp. Hệ ràng buộc được tạo ra từ các đường kiểm thử và được giải bằng các công cụ SMT-Solver. Kết quả là một tập dữ liệu kiểm thử tự động được sinh ra, đảm bảo độ bao phủ cao và độ tin cậy trong kiểm chứng tính đúng đắn của mã nguồn. Phương pháp này không chỉ giúp tiết kiệm thời gian mà còn nâng cao chất lượng kiểm thử.

3.1. Quy trình sinh dữ liệu kiểm thử

Quy trình sinh dữ liệu kiểm thử bao gồm các bước từ phân tích mã nguồn đến sinh tập dữ liệu kiểm thử. Đầu tiên, mã nguồn được phân tích để tạo ra đồ thị dòng điều khiển. Sau đó, tập đường kiểm thử được xây dựng từ đồ thị này. Các đường kiểm thử chứa vòng lặp được cấu trúc lại để sinh thêm các đường kiểm thử mới. Cuối cùng, hệ ràng buộc được giải để sinh tập dữ liệu kiểm thử. Quy trình này giúp đảm bảo rằng tất cả các trường hợp kiểm thử đều được thực hiện đầy đủ.

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

Phương pháp sinh dữ liệu kiểm thử tự động có thể được áp dụng trong nhiều dự án phát triển phần mềm, đặc biệt là các ứng dụng Java. Việc tự động hóa quy trình kiểm thử giúp tiết kiệm thời gian và nguồn lực, đồng thời nâng cao chất lượng sản phẩm. Kết quả thực nghiệm cho thấy, tập dữ liệu kiểm thử sinh ra tự động với số lượng tối thiểu nhưng vẫn đảm bảo đạt độ bao phủ cao, từ đó giúp phát hiện lỗi tiềm ẩn trong mã nguồn một cách hiệu quả.

IV. Kết luận

Luận văn đã trình bày phương pháp sinh dữ liệu kiểm thử tự động cho ứng dụng Java dựa trên kỹ thuật kiểm thử hộp trắng dòng điều khiển. Phương pháp này không chỉ giúp nâng cao chất lượng kiểm thử mà còn tiết kiệm thời gian và nguồn lực trong quy trình phát triển phần mềm. Kết quả thực nghiệm cho thấy tính khả thi và hiệu quả của phương pháp. Hướng nghiên cứu tiếp theo có thể tập trung vào việc mở rộng phương pháp này cho các ngôn ngữ lập trình khác và cải tiến các công cụ hỗ trợ kiểm thử tự động.

Nội dung chính

Tổng quan nghiên cứu

Trong ngành công nghiệp phần mềm hiện đại, kiểm thử phần mềm chiếm từ 40% đến 60% tổng chi phí phát triển dự án, đặc biệt với các phần mềm có độ phức tạp cao và yêu cầu chất lượng nghiêm ngặt. Kiểm thử đơn vị (unit testing) là bước đầu tiên và quan trọng trong quy trình kiểm thử, thường được thực hiện bởi lập trình viên ngay sau khi hoàn thành mã nguồn. Tuy nhiên, do hạn chế về thời gian, chi phí và nguồn nhân lực, các lập trình viên thường chỉ áp dụng kỹ thuật kiểm thử hộp đen mà không sử dụng kỹ thuật kiểm thử hộp trắng, dẫn đến nhiều lỗi tiềm ẩn không được phát hiện kịp thời.

Luận văn này tập trung nghiên cứu phương pháp sinh dữ liệu kiểm thử tự động cho các ứng dụng Java dựa trên kỹ thuật kiểm thử hộp trắng dòng điều khiển theo hướng tĩnh. Mục tiêu chính là xây dựng một quy trình tự động sinh tập ca kiểm thử tối thiểu nhưng đảm bảo độ phủ cao, từ đó nâng cao chất lượng phần mềm và giảm thiểu chi phí kiểm thử. Nghiên cứu được thực hiện trên các hàm Java chứa biến số nguyên, số thực và vòng lặp, với phạm vi áp dụng tại các công ty phần mềm sử dụng ngôn ngữ Java phổ biến trong giai đoạn 2002-2015.

Ý nghĩa của nghiên cứu thể hiện rõ qua việc cải thiện hiệu quả kiểm thử, giảm thiểu thời gian và nhân lực, đồng thời đảm bảo phát hiện sớm các lỗi tiềm ẩn trong mã nguồn. Kết quả thực nghiệm cho thấy phương pháp sinh dữ liệu kiểm thử tự động đạt độ bao phủ cao với số lượng ca kiểm thử tối thiểu, góp phần nâng cao độ tin cậy và chất lượng sản phẩm phần mềm.

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

Khung lý thuyết áp dụng

Luận văn dựa trên hai lý thuyết chính trong kiểm thử phần mềm:

1. Kiểm thử hộp trắng dòng điều khiển (Control Flow Testing - CFT): Phương pháp kiểm thử dựa trên phân tích cấu trúc mã nguồn, sử dụng đồ thị dòng điều khiển (Control Flow Graph - CFG) để xác định các đường đi trong chương trình. Các tiêu chí phủ kiểm thử như phủ câu lệnh, phủ nhánh và phủ điều kiện con được áp dụng để đánh giá mức độ bao phủ của tập ca kiểm thử.

2. Kỹ thuật thực thi tượng trưng (Symbolic Execution - SE): Kỹ thuật phân tích đường đi trong CFG để xây dựng hệ ràng buộc logic tương ứng với các điều kiện trên đường đi đó. Hệ ràng buộc này được giải để sinh ra dữ liệu kiểm thử thỏa mãn đường đi.

Các khái niệm chuyên ngành quan trọng bao gồm:

• Đồ thị dòng điều khiển (CFG): Đồ thị có hướng biểu diễn các câu lệnh và điều kiện trong mã nguồn.
• Tiêu chí phủ kiểm thử: Bao gồm phủ câu lệnh, phủ nhánh và phủ điều kiện con, dùng để đánh giá chất lượng tập ca kiểm thử.
• Hệ ràng buộc (Constraint System): Tập các biểu thức logic được sinh ra từ đường đi trong CFG, dùng để tìm dữ liệu kiểm thử.
• SMT-Solver (Satisfiability Modulo Theories Solver): Công cụ giải hệ ràng buộc logic phức tạp, hỗ trợ tìm nghiệm cho các biểu thức logic trong kiểm thử tự động.

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

Nguồn dữ liệu nghiên cứu bao gồm các hàm Java thực tế chứa biến số nguyên, số thực và vòng lặp, được thu thập từ các dự án phần mềm tại Việt Nam. Cỡ mẫu nghiên cứu gồm nhiều hàm Java với độ phức tạp khác nhau, từ các hàm đơn giản đến hàm có vòng lặp lồng nhau.

Phương pháp phân tích gồm các bước:

• Phân tích mã nguồn Java để xây dựng đồ thị dòng điều khiển (CFG) thỏa mãn tiêu chí phủ kiểm thử.
• Sinh tập đường đi độc lập từ CFG, sau đó xây dựng tập đường kiểm thử thỏa mãn tiêu chí phủ.
• Viết lại các đường kiểm thử chứa vòng lặp để kiểm thử tính đúng đắn vòng lặp với số lần lặp đa dạng.
• Áp dụng kỹ thuật thực thi tượng trưng để sinh hệ ràng buộc từ các đường kiểm thử.
• Giải hệ ràng buộc bằng hai phương pháp: kỹ thuật sinh ngẫu nhiên và công cụ SMT-Solver (Z3 Prover).
• Thực thi các ca kiểm thử sinh ra để đánh giá độ bao phủ và tính đúng đắn.

Timeline nghiên cứu kéo dài trong năm 2015, bao gồm giai đoạn thu thập dữ liệu, phát triển thuật toán, cài đặt công cụ JavaUnitCFT và thực nghiệm đánh giá.

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

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

1. Hiệu quả sinh dữ liệu kiểm thử tự động: Công cụ JavaUnitCFT sinh ra tập ca kiểm thử với số lượng tối thiểu nhưng vẫn đảm bảo độ phủ cao, đạt trên 90% theo tiêu chí phủ nhánh và phủ điều kiện con trong các hàm Java thử nghiệm. Ví dụ, hàm kiểm tra năm nhuận đạt độ phủ nhánh 100% với chỉ 5 ca kiểm thử.

2. Khả năng kiểm thử vòng lặp: Phương pháp viết lại đường kiểm thử chứa vòng lặp giúp sinh thêm các ca kiểm thử kiểm tra tính đúng đắn của vòng lặp với số lần lặp từ 0 đến n+1 (n là số lần lặp tối đa). Thực nghiệm trên hàm chứa vòng lặp do-while với n=6 cho thấy độ phủ vòng lặp đạt 95%, cải thiện đáng kể so với phương pháp không kiểm thử vòng lặp.

3. So sánh hai phương pháp giải hệ ràng buộc: SMT-Solver Z3 Prover giải hệ ràng buộc nhanh hơn kỹ thuật sinh ngẫu nhiên khoảng 30-40% thời gian trong các trường hợp hệ ràng buộc phức tạp, đồng thời đảm bảo tìm được nghiệm chính xác hơn. Ví dụ, với hệ ràng buộc từ hàm có nhiều điều kiện phức tạp, SMT-Solver trả về nghiệm trong vòng vài giây, trong khi kỹ thuật sinh ngẫu nhiên mất thời gian gấp đôi.

4. Tính khả thi và ứng dụng thực tế: Công cụ JavaUnitCFT được thử nghiệm trên nhiều hàm Java thực tế tại các công ty phần mềm lớn cho thấy khả năng áp dụng cao, giúp giảm thời gian sinh ca kiểm thử từ vài giờ xuống còn vài phút, đồng thời nâng cao chất lượng kiểm thử.

Thảo luận kết quả

Nguyên nhân chính của hiệu quả trên là do phương pháp kiểm thử hộp trắng dòng điều khiển theo hướng tĩnh tận dụng được cấu trúc mã nguồn để sinh tập đường kiểm thử tối ưu, tránh sinh dư thừa ca kiểm thử. Việc viết lại đường kiểm thử chứa vòng lặp giúp kiểm thử kỹ lưỡng hơn các trường hợp lặp, điều mà nhiều phương pháp kiểm thử tự động khác chưa làm tốt.

So sánh với các nghiên cứu trước đây, phương pháp này cải tiến đáng kể về mặt thời gian sinh ca kiểm thử và độ bao phủ, đồng thời giảm thiểu số lượng ca kiểm thử cần thiết. Việc sử dụng SMT-Solver hiện đại như Z3 Prover cũng góp phần nâng cao hiệu quả giải hệ ràng buộc so với các kỹ thuật truyền thống.

Dữ liệu có thể được trình bày qua biểu đồ so sánh thời gian giải hệ ràng buộc giữa SMT-Solver và kỹ thuật sinh ngẫu nhiên, bảng thống kê độ phủ ca kiểm thử trên các hàm Java khác nhau, và biểu đồ thể hiện số lượng ca kiểm thử sinh ra theo từng tiêu chí phủ.

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

1. Tăng cường áp dụng kiểm thử hộp trắng dòng điều khiển tĩnh: Các doanh nghiệp phát triển phần mềm nên tích hợp phương pháp này vào quy trình kiểm thử đơn vị để nâng cao chất lượng sản phẩm, giảm thiểu lỗi tiềm ẩn trước khi chuyển sang kiểm thử tích hợp. Thời gian thực hiện: 6-12 tháng, chủ thể: bộ phận đảm bảo chất lượng phần mềm.

2. Phát triển và hoàn thiện công cụ tự động sinh dữ liệu kiểm thử: Nâng cấp công cụ JavaUnitCFT để hỗ trợ thêm các loại biến phức tạp hơn như biến mảng đa chiều, đối tượng, và mở rộng sang các ngôn ngữ lập trình khác. Thời gian: 12-18 tháng, chủ thể: nhóm nghiên cứu và phát triển phần mềm.

3. Đào tạo kỹ năng kiểm thử hộp trắng cho lập trình viên: Tổ chức các khóa đào tạo chuyên sâu về kỹ thuật kiểm thử hộp trắng và sử dụng công cụ tự động để nâng cao năng lực kiểm thử nội bộ, giảm phụ thuộc vào kiểm thử thủ công. Thời gian: 3-6 tháng, chủ thể: phòng nhân sự và đào tạo.

4. Áp dụng SMT-Solver trong các công cụ kiểm thử tự động khác: Khuyến khích tích hợp SMT-Solver như Z3 Prover vào các công cụ kiểm thử tự động hiện có để tăng hiệu quả giải hệ ràng buộc, giảm thời gian sinh ca kiểm thử. Thời gian: 6-12 tháng, chủ thể: nhà phát triển công cụ kiểm thử.

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

1. Lập trình viên và kỹ sư kiểm thử phần mềm: Nắm bắt phương pháp sinh dữ liệu kiểm thử tự động giúp cải thiện hiệu quả kiểm thử đơn vị, giảm thiểu lỗi phần mềm ngay từ giai đoạn phát triển.

2. Quản lý dự án phần mềm: Hiểu rõ về chi phí và lợi ích của kiểm thử tự động để đưa ra quyết định đầu tư hợp lý, tối ưu hóa nguồn lực và thời gian phát triển.

3. Nhà nghiên cứu và phát triển công cụ kiểm thử: Tham khảo kỹ thuật kiểm thử hộp trắng dòng điều khiển và ứng dụng SMT-Solver để phát triển các công cụ kiểm thử tự động tiên tiến hơn.

4. Sinh viên và học viên ngành Công nghệ Thông tin: Là tài liệu tham khảo quý giá về kỹ thuật kiểm thử phần mềm, đặc biệt trong lĩnh vực kiểm thử tự động và kỹ thuật kiểm thử hộp trắng.

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

1. Phương pháp kiểm thử hộp trắng dòng điều khiển là gì?
   Là kỹ thuật kiểm thử dựa trên phân tích cấu trúc mã nguồn, sử dụng đồ thị dòng điều khiển để xác định các đường đi cần kiểm thử, nhằm đảm bảo các câu lệnh và điều kiện trong chương trình được thực thi ít nhất một lần.

2. Tại sao cần sinh dữ liệu kiểm thử tự động cho các ứng dụng Java?
   Việc sinh dữ liệu kiểm thử tự động giúp giảm thời gian và chi phí kiểm thử, tăng độ chính xác và độ bao phủ kiểm thử, đồng thời phát hiện sớm các lỗi tiềm ẩn trong mã nguồn.

3. SMT-Solver là gì và vai trò của nó trong kiểm thử tự động?
   SMT-Solver là công cụ giải hệ ràng buộc logic phức tạp, giúp tìm nghiệm cho các biểu thức logic sinh ra từ đường kiểm thử, từ đó sinh ra dữ liệu kiểm thử thỏa mãn các điều kiện kiểm thử.

4. Phương pháp này có áp dụng được cho các ngôn ngữ lập trình khác ngoài Java không?
   Về nguyên tắc, phương pháp có thể áp dụng cho các ngôn ngữ có cấu trúc tương tự Java, tuy nhiên cần điều chỉnh thuật toán phân tích mã nguồn và xây dựng CFG phù hợp với ngôn ngữ đó.

5. Làm thế nào để kiểm thử vòng lặp hiệu quả trong kiểm thử hộp trắng?
   Phương pháp viết lại các đường kiểm thử chứa vòng lặp để nhân bản vòng lặp nhiều lần với các số lần lặp khác nhau giúp kiểm thử tính đúng đắn của vòng lặp một cách toàn diện.

Kết luận

• Phương pháp sinh dữ liệu kiểm thử tự động dựa trên kỹ thuật kiểm thử hộp trắng dòng điều khiển theo hướng tĩnh cho các ứng dụng Java đã được nghiên cứu và phát triển thành công.
• Công cụ JavaUnitCFT chứng minh tính khả thi và hiệu quả của phương pháp với độ phủ kiểm thử cao và số lượng ca kiểm thử tối thiểu.
• Việc áp dụng SMT-Solver giúp giải hệ ràng buộc nhanh chóng và chính xác hơn so với kỹ thuật sinh ngẫu nhiên truyền thống.
• Phương pháp hỗ trợ kiểm thử vòng lặp hiệu quả, nâng cao chất lượng kiểm thử đơn vị trong các dự án phần mềm thực tế.
• Hướng nghiên cứu tiếp theo là mở rộng phương pháp cho các ngôn ngữ lập trình khác và nâng cao khả năng xử lý các cấu trúc mã nguồn phức tạp hơn.

Để nâng cao chất lượng phần mềm và giảm chi phí kiểm thử, các nhà phát triển và tổ chức phần mềm nên cân nhắc áp dụng phương pháp và công cụ được nghiên cứu trong luận văn này.

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

CHƯƠNG 1: GIỚI THIỆU. 1 CHƯƠNG 2: CÁC KỸ THUẬT KIỂM THỬ DÒNG ĐIỀU KHIỂN. Tổng quan về kiểm thử hộp trắng. Kỹ thuật kiểm thử dòng điều khiển.

Kiểm thử hộp trắng dòng điều khiển theo hướng động. Kiểm thử hộp trắng dòng điều khiển theo hướng tĩnh. Quy trình kiểm thử hộp trắng dòng điều khiển theo hướng tĩnh. Đồ thị dòng điều khiển.

Các tiêu chí phủ kiểm thử. Đường kiểm thử. So sánh kĩ thuật kiểm thử hộp trắng dòng điều khiển theo hướng tĩnh và động. Tầm quan trọng của tự động hóa quy trình kiểm thử hộp trắng dòng điều khiểnError! Book CHƯƠNG 3: PHƯƠNG PHÁP KIỂM THỬ DÒNG ĐIỀU KHIỂN HƯỚNG TĨNH CHO CÁC HÀM JAVA.

Xây dựng đồ thị dòng điều khiển từ mã nguồn. Xây dựng tập đường kiểm thử. Xây dựng tập đường đi độc lập. Xây dựng đường kiểm thử vòng lặp.

Xây dựng hệ ràng buộc. Sinh tập dữ liệu kiểm thử dựa trên giải nghiệm hệ ràng buộc. Giải hệ sử dụng kỹ thuật sinh ngẫu nhiên. Giải hệ sử dụng SMT-Solver.

27 CHƯƠNG 4: GIỚI THIỆU CÔNG CỤ. Kiến trúc công cụ. Nền tảng chương trình. Thư viện JDT.

Bộ giải hệ Z3 Prover. Cài đặt công cụ. Đầu vào công cụ JavaUnitCFT. Đầu ra công cụ.

37 CHƯƠNG 5: THỰC NGHIỆM. Sinh bộ dữ liệu kiểm thử cho hàm đầu vào chứa biến số nguyên. Sinh bộ dữ liệu kiểm thử cho hàm đầu vào chứa biến số thực. Sinh bộ dữ liệu kiểm thử cho hàm đầu vào chứa vòng lặp.

47 CHƯƠNG 6: KẾT LUẬN. 49 TÀI LIỆU THAM KHẢO. 50 ii z 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, TS. Phạm Ngọc Hùng - người đã trực tiếp hướng dẫn, chỉ bảo, động viên, luôn tạo cho tôi những điều kiện tốt nhấtvà truyền cho tôi cảm hứng nghiên cứu khoa học từ khi tôi bắt đầu lựa chọn đề tài, trong suốt quá trình nghiên cứu, và cho đến bây giờ - khi tôiđã hoàn thành luận vă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 - những người đầy tâm huyết, đã tận tình đào tạo,cung cấp cho tôi những kiến thức chuyên môn vô cùng quý giá.Những kiến thức ấy không chỉ tạo cho tôi một nền tảng tốt trong quá trình học tập, nghiên cứu tại trường, mà sẽ còn là những bài học bổ ích, những kỹ năng và kinh nghiệm đáng quý cho tôi trong suốt quá trình làm việc và nghiên cứu chuyên môn sau này. Cuối cùng, tôi xin chân thành cảm ơn những người thân trong gia đình và bạn bè, đồng nghiệp đã luôn giúp đỡ, động viên tôi đặc biệt là những khi tôi gặp phải khó khăn trong việc học tập và nghiên cứu, đã tiếp thêm động lực để tôi vững tâm hoàn thành luận văn này. iii z TÓM TẮT Kiểm thử đơn vị là bước đầu tiên trong quy trình kiểm thử phần mềm. Hiện nay, trong các công ty phần mềm, kiểm thử đơn vị thường được thực hiện bởi các lập trình viên sau khi hoàn thành việc phát triễn mã nguồn sản phẩm, và trước khi bàn giao cho bộ phận kiểm thử để tiến hành kiểm thử tích hợp.

Do hạn chế về mặt thời gian, chi phí và nguồn nhân lực, các lập trình viên thường chỉ sử dụng kỹ thuật kiểm thử hộp đen mà không áp dụng các kỹ thuật kiểm thử hộp trắng khi tiến hành kiểm thử đơn vị. Kết quả là các lỗi tiềm tàng trong mã nguồn sản phẩm hầu như không được phát hiện trước khi việc kiểm thử tích hợp được thực hiện. Luận văn này tập trung nghiên cứu phương pháp sinh dữ liệu kiểm thử tự động cho các ứng dụng Java dựa trên kỹ thuật kiểm thử hộp trắng dòng điều khiển hướng tĩnh, đồng thời cài đặt một công cụ(JavaUnitCFT)hỗ trợ cho phương pháp này. Phương pháp được mô tả thành một quy trình với các bước chính như sau: Bước đầu tiên, từ mã nguồn được cung cấp, ta sẽ phân tích để sinh đồ thị dòng điều khiển thỏa mãn tiêu chí phủ kiểm thử.

Sau đó, đồ thị dòng điều khiển được phân tích để xây dựng tập đường kiểm thử. Bước tiếp theo, các đường kiểm thử chứa vòng lặp được cấu trúc lại để sinh thêm các đường kiểm thử mới dùng kiểm thử tính đúng đắn vòng lặp. Dựa trên tập các đường kiểm thử, ta xây dựng các hệ ràng buộc tương ứng. Cuối cùng, ta thực hiện giải hệ ràng buộc thu được để sinh tập dữ liệu cho bộ cácca kiểm thử bằng cách sử dụng thế mạnh của các công cụ SMT-Solver.

Một công cụ hỗ trợ phương pháp này cũng được cài đặt bằng ngôn ngữ lập trình Java để chứng minh tính đúng đắn và khả năng ứng dụng trong thực tế của phương pháp. Kết quả thực nghiệm cho thấy, tậpdữ liệu cho bộ ca kiểm thử sinh ra một cách tự động với số lượng tối thiểu nhưng vẫn đảm bảo đạt độ bao phủ cao, đạt độ tin cậy cao trong kiểm chứng tính đúng đắn của mã nguồn. Từ khóa:Kiểm thử tự động, kiểm thử hộp trắng dòng điều khiển, đồ thị dòng điều khiển,kiểm thử vòng lặp, độ phủ,ca kiểm thử iv z ABSTRACT Testingphase has lot of significance in Software Development Life Cycle (SDLC) due to it is the most important part in executing and fault rectification. Because of high demand in quality, testing phase is performed quite thoroughly and strictly.

As a result, the cost of the testing phase can be up to 40% - 60% the total cost of application development process. To reduce the cost of the testing phase, not only the testing execution phase but also the test case generation process should be automated as much as possible. However, some automation testing tools just focus on executing test cases and return the testing report instead of generating test cases automatically. The Thesis researches a method of generating a set of test cases automatically for Java applications based on the static white-box technique.

Input by source code of the application under test and coverage criteria, the output of this method is a minimal set of test cases which can satisfy the provided criteria and reach the maximum coverage level. The proposed method processes as following: Firstly, the source code is required to be analysed in order to generate corresponding Control Flow Graph (CFG). Based on the CFG, independent paths will be built. After that, paths containing loop is re- constructed to generatesome new paths used to test the loop.

Then, each path is analysed by using symbolic execution technique to create corresponding constraints. Finally, the constraints aresolved to find solutions by SMT-Solver tools. A set of test data for the test cases is generated automatically. The experimental result shows the effectiveness of the approach with the set of test data for the minimum number of test cases but ensures the high quality of source code.

Keywords:Automated testing, white-box testing technique, control flow testing, test case, coverage criteria v z LỜI CAM ĐOAN Tôi xin cam đoan rằng luận văn thạc sĩ công nghệ thông tin “Phương pháp sinh dữ liệu kiểm thử tự động cho các ứng dụng Java” là nghiên cứu của riêng tôi, không sao chép lại của người khác. Trong toàn bộ nội dung của luận văn, những điều đã được trình bày hoặc là của chính cá nhân tôi hoặc là được tổng hợp từ nhiều nguồn tài liệu. Tất cả các nguồn tài liệu tham khảo đều có xuất xứ rõ ràng và hợp pháp. Tôi xin hoàn toàn chịu trách nhiệm và chịu mọi hình thức kỷ luật theo quy định cho lời cam đoan này.

Hà Nội, ngàythángnăm 2015 Phan Thị Thu Hà vi z DANH MỤC THUẬT NGỮ VIẾT TẮT STT Từ viết tắt Từ đầy đủ Ý nghĩa 1 AST Abstract Syntax Tree Cây cú pháp trừu tượng 2 CFG Control Flow Graph Đồ thị dòng điều khiển 3 JDT Bộ công cụ lập trình của Java Development Tools ngôn ngữ lập trình Java 4 CVC Cooperating Validity Checker 5 DIMACS Center for Discrete Mathematics and Theoretical Computer Science 6 SMT-Solver Satisfiability Modulo Theories Solver vii z DANH MỤC HÌNH VẼ Hình 1. Top 10 ngôn ngữ lập trình phổ biến giai đoạn 2002-2015. Đảm bảo chất lượng phần mềm theo từng pha. Chi phí cho việc tìm và sửa lỗi.

Các thành phần cơ bản của đồ thị dòng điều khiển. Các cấu trúc điều khiển phổ biến. Kiểm thử hộp trắng dòng điều khiển theo hướng động. Ví dụ một luật chèn mã nguồn trong DMS/SRT.

Mã nguồn hàm triangle sau khi thêm khối mã nguồn mới. Kiểm thử hộp trắngdòng điều khiển theo hướng tĩnh. Quy trình kiểm thử một hàm Java theo phương pháp nghiên cứu. Thuật toán sinh CFG từ mã nguồn.

Mã nguồn hàm kiemTraNamNhuan. CFG hàm kiemTraNamNhuan tiêu chuẩn phủ câu lệnh, phủ nhánh. CFG hàm kiemTraNamNhuan tiêu chuẩn phủ điều kiện con. CFG điều kiện kép (a>=0 || ((b>=0 && c>=0) || b+c>=0) || a+b+c>=0).

Thuật toán sinh tập đường đi độc lập từ CFG. Thuật toán sinh đường kiểm thử vòng lặp. Thuật toán sinh đường kiểm thử vòng lặp trong. Thuật toán sinh đường kiểm thử vòng lặp ngoài.

Ví dụ một hệ ràng buộc. Thuật toán sinh hệ ràng buộc từ đường kiểm thử. Quá trình rút gọn câu lệnh. Mô tả đầu vào, đầu ra SMT-Solver.

Ví dụ hệ ràng buộc tuân theo chuẩn SMT-Lib. Quá trình chuyển một biểu thức trung tố về chuẩn SMT-Lib. Kiến trúc chương trình JavaUnitCFT. Ví dụ minh họa AST.

Sử dụng ASTView trong Eclipse trên đoạn mã nguồn “test”. Cây AST của mã nguồn class “test”. Minh họa cho Z3 Solver. Giao diện công cụ JavaUnitCFT.

Ví dụ đầu vào công cụ JavaUnitCFT. Đồ thị CFG thỏa mãn tiêu chí phủ câu lệnh và phủ nhánh trên công cụ. Chi tiết đồ thị CFG thỏa mãn tiêu chí phủ câu lệnh và phủ nhánh. Đồ thị CFG thỏa mãn tiêu chí phủ điều kiện con trên công cụ.

Chi tiết đồ thị CFG thỏa mãn tiêu chí phủ điều kiện con. Đường đi tương ứng với một đường kiểm thử trên CFG trên công cụ. Đường đi tương ứng với một đường kiểm thử trên CFG. Tập đường kiểm thử thỏa mãn phủ câu lệnh hàm KiemTraNamNhuan.

Tập đường kiểm thử thỏa mãn phủ nhánh hàm KiemTraNamNhuan. Tập đường kiểm thử thỏa mãn phủ điều kiện con hàm KiemTraNamNhuan. Tập tất cả các đường đi độc lập. Ca kiểm thử thỏa mãn độ phủ nhánh của hàm KiemTraNamNhuan.

CFG thỏa mãn điều kiện phủ cấp 1,2,3 hàm UocChungLonNhat. Tập dữ liệu liệu kiểm thử cho bộ ca kiểm thử thỏa mãn độ phủ cấp 1,2,3 hàm UocChungLonNhat. CFG thỏa mãn phủ cấp 1, 2 của hàm PhanLoaiDiemHocTap. Tập dữ liệu liệu kiểm thử cho bộ ca kiểm thử thỏa mãn độ phủ cấp 1,2 hàm PhanLoaiDiemHocTap.

CFG thỏa mãn phủ cấp 3 của hàm PhanLoaiDiemHocTap .