ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ Nguyễn Đức Anh PHƯƠNG PHÁP PHÂN TÍCH MÃ NGUỒN VÀ SINH DỮ LIỆU KIỂM THỬ CHO CÁC DỰ ÁN C/C++ LUẬN VĂN THẠC SĨ: KỸ THUẬT PHẦN MỀM HÀ NỘI – 2017 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com I ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ Nguyễn Đức Anh PHƯƠNG PHÁP PHÂN TÍCH MÃ NGUỒN VÀ SINH DỮ LIỆU KIỂM THỬ CHO CÁC DỰ ÁN C/C++ Ngành: Công nghệ thông tin Chuyên ngành: Kỹ thuật phần mềm Mã số: 60480103 LUẬN VĂN THẠC SĨ: KỸ THUẬT PHẦN MỀM Cán bộ hướng dẫn: PGS. Phạm Ngọc Hùng HÀ NỘI - 2017 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com II LỜI CẢM ƠN Đầu tiên, tôi xin gửi lời cám ơn chân thành tới Tiến sĩ Phạm Ngọc Hùng – giảng viên bộ môn Công Nghệ Phần Mềm – người đã hướng dẫn tận tình, tỉ mỉ, chu đáo tôi trong suốt hai năm làm luận văn. Quãng thời gian được thầy hướng dẫn đã giúp tôi học hỏi, đúc kết được nhiều kinh nghiệm về phương pháp nghiên cứu, kĩ năng giao tiếp, kĩ năng làm việc nhóm, kĩ năng trình bày. Thầy còn truyền cho tôi ngọn lửa yêu nghiên cứu khoa học, niềm tin vượt qua những khó khăn trong cuộc sống và dạy tôi cách vượt qua những khó khăn đó.
Tôi cảm thấy tự hào và may mắn khi là một học viên được thầy hướng dẫn trong những năm tháng cao học. Ngoài ra, tôi xin gửi lời cám ơn chân thành đến nhóm nghiên cứu đã giúp đỡ tôi nhiệt tình để hoàn thành luận văn sao cho đạt hiệu quả cao nhất. Cám ơn nhóm nghiên cứu đã giúp đỡ tôi bằng hành động, bằng lời nói mỗi khi tôi gặp khó khăn, thất bại. Hai năm bên nhau không phải là dài nhưng đối với tôi, đây là quãng thời gian tuyệt vời nhất và không thể nào quên.
Tiếp theo, tôi xin gửi lời cảm ơn đến các thầy cô giảng viên Trường Đại học Công Nghệ - Đại học Quốc Gia Hà Nội – những người đã tận tâm truyền đạt những kiến thức quý báu làm nền tảng để tôi tiếp tục đi xa hơn nữa trong lĩnh vực công nghệ thông tin. Cuối cùng, tôi xin được cảm ơn gia đình đã nuôi tôi khôn lớn để trở thành người có ích cho xã hội, giúp tôi có một điểm tựa vững chắc để yên tâm học hành trong suốt bao năm qua. Tôi xin gửi lời cám ơn chân thành tới cha, mẹ, em gái đã luôn động viên và cổ vũ tôi mỗi khi tôi gặp khó khăn và thử thách. Hà Nội, ngày 25 tháng 11 năm 2017 Học viên Nguyễn Đức Anh LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com III LỜI CAM ĐOAN Tôi xin cam đoan rằng những nghiên cứu về kiểm thử tự động cho chương trình C/C++ được trình bày trong luận văn này là của tôi và chưa từng được nộp như một báo cáo luận văn tại trường Đại học Công Nghệ - Đại học Quốc Gia Hà Nội hoặc bất kỳ trường đại học khác.
Những gì tôi viết ra không sao chép từ các tài liệu, không sử dụng các kết quả của người khác mà không trích dẫn cụ thể. Tôi xin cam đoan công cụ kiểm thử tự động tôi trình bày trong khoá luận là do tôi tự phát triển, không sao chép mã nguồn của người khác. Nếu sai tôi hoàn toàn chịu trách nhiệm theo quy định của trường Đại học Công Nghệ - Đại học Quốc Gia Hà Nội. Hà Nội, ngày 25 tháng 11 năm 2017 Học viên Nguyễn Đức Anh LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com IV MỤC LỤC Giới thiệu.
1 Tổng quan kĩ thuật kiểm thử tự động định hướng. Dữ liệu kiểm thử. Các tiêu chí độ phủ sử dụng trong kĩ thuật kiểm thử tự động định hướng 5 2. Đồ thị dòng điều khiển.
Cây cú pháp trừu tượng. Quy trình chung kĩ thuật kiểm thử tự động định hướng. 7 Phương pháp kiểm thử tự động dự án C/C++ sử dụng kĨ thuật kiểm thử tự động định hướng. Tổng quan phương pháp đề xuất.
Pha tiền xử lý mã nguồn. Xây dựng cây cấu trúc từ dự án C/C++. Chèn các câu lệnh đánh dấu vào hàm. Pha sinh dữ liệu kiểm thử.
Xây dựng đồ thị dòng điều khiển từ mã nguồn. Xếp hạng đường thi hành. Xây dựng hệ ràng buộc từ đường thi hành. Mô hình bộ nhớ sử dụng trong kĩ thuật thực thi tượng trưng.
Xây dựng hệ ràng buộc từ đường thi hành sử dụng kĩ thuật thực thi tượng trưng. Giải hệ ràng buộc sử dụng bộ giải SMT-Solver. Biên dịch và thực thi dữ liệu kiểm thử trong môi trường chạy. Tối ưu hóa pha sinh dữ liệu kiểm thử.
Đơn giản hóa hệ ràng buộc. 27 LUAN VAN CHAT LUONG download : add luanvanchat@agmail. Tăng tốc thời gian biên dịch và thực thi dữ liệu kiểm thử. Xuất mã nguồn kiểm thử theo chuẩn Google Test.
29 Công cụ và thực nghiệm. Giới thiệu công cụ kiểm thử tự động CFT4Cpp. Thư viện hỗ trợ sử dụng trong công cụ kiểm thử tự động CFT4Cpp. Thư viện giải hệ ràng buộc Z3.
Thư viện phân tích mã nguồn CDT. Thư viện tính giá trị biểu thức Jeval. Kết quả thực nghiệm. So sánh số lượng bộ dữ liệu kiểm thử và độ phủ với KLEE, CAUT, CREST, PathCrawler.
Sinh dữ liệu kiểm thử vòng lặp. So sánh thời gian biên dịch và thực thi dữ liệu kiểm thử. 44 Tài liệu tham khảo. 48 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com VI DANH SÁCH KÝ HIỆU, CHỮ VIẾT TẮT Tên đầy đủ Tên viết tắt Mô tả Dynamic Symbolic Execution DSE Kĩ thuật kiểm thử động Static Testing Kĩ thuật kiểm thử tĩnh Concolic Testing Kĩ thuật kiểm thử tự động định hướng Abstract Syntax Tree AST Cây cú pháp trừu tượng Control Flow Graph CFG Đồ thị dòng điều khiển C/C++ Development Tooling CDT Satisfiability Modulo Theories SMT-Solver Solver Boolean Satisfiability Problem SAT Symbolic Execution SE Kĩ thuật thực thi tượng trưng Chiến thuật chọn đường thi hành (trong Path selection strategy DSE) Test driver Bộ thực thi dữ liệu kiểm thử Test data Dữ liệu kiểm thử Test path Đường thi hành (sinh từ đồ thị CFG) Modified condition/ decision MC/DC Độ phủ cấp ba (hoặc phủ điều kiện con) coverage LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com VII DANH SÁCH BẢNG BIỂU Bảng 3.
Danh sách quan hệ phụ thuộc lô-gic điển hình. Luật chèn câu lệnh đánh dấu vào hàm. Thông tin các công cụ so sánh trong thực nghiệm. Thông tin cấu hình các ví dụ trong thực nghiệm.
Thông tin các hàm kiểm thử về tiêu chí độ phủ và số bộ dữ liệu kiểm thử. Kết quả so sánh công cụ CFT4Cpp với KLEE và PathCrawler. Kết quả so sánh công cụ CFT4Cpp với CREST và CAUT. Sinh dữ liệu kiểm thử vòng lặp.
Bảng so sánh thời gian biên dịch và thực thi dữ liệu kiểm thử giữa kĩ thuật cải tiến và kĩ thuật truyền thống. 43 DANH SÁCH THUẬT TOÁN Thuật toán 3. Thuật toán LDFS sinh dữ liệu kiểm thử. Thuật toán xây dựng hệ ràng buộc từ đường thi hành.
23 DANH SÁCH HÌNH VẼ Hình 2. Các cấu trúc điều khiển phổ biến trong C/C++. Tổng quan phương pháp đề xuất. Ví dụ cây cấu trúc của một dự án C/C++ điển hình.
Minh họa đồ thị CFG phủ câu lệnh/nhánh. Minh họa đồ thị CFG phủ MC/DC. Mô hình bộ nhớ sử dụng trong kĩ thuật thực thi tượng trưng. Quy trình xây dựng biểu thức SMT-Lib từ ràng buộc.
Quá trình biến đổi hệ ràng buộc về chuẩn SMTLib. Kĩ thuật tạo bộ thực thi ca kiểm thử tổng quát. 28 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com VIII Hình 4. Kiến trúc công cụ CFT4Cpp.
Giao diện chính của công cụ CFT4Cpp. Giao diện bước cấu hình công cụ CFT4Cpp. Giao diện sinh dữ liệu kiểm thử cho hàm Divide. Biên bản kiểm thử xuất bởi công cụ CFT4Cpp cho hàm Divide.
Minh họa kết quả giải hệ ràng buộc sử dụng Z3. 34 DANH SÁCH MÃ NGUỒN Mã nguồn 3. Ví dụ một phần mã nguồn trong dự án C/C++. Ví dụ hàm checkFirstSubject sau khi chèn câu lệnh đánh dấu.
Mã nguồn hàm average. Minh họa một hệ ràng buộc theo chuẩn SMT-Lib. 34 LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com IX TÓM TẮT Để đảm bảo chất lượng phần mềm, nhiều kĩ thuật kiểm thử khác nhau được áp dụng khiến chi phí kiểm thử tăng cao. Trong đó, kiểm thử đơn vị là một trong những kĩ thuật được áp dụng rộng rãi trong các công ty phần mềm để kiểm tra chất lượng mã nguồn, đặc biệt đối với các phần mềm nhúng viết bằng ngôn ngữ C/C++.
Kĩ thuật này giúp phát hiện sớm nhiều vấn đề tiềm ẩn trong quy trình xây dựng phần mềm. Tuy nhiên, nhược điểm của kĩ thuật kiểm thử đơn vị là vấn đề chi phí tăng cao đối với những dự án lớn bởi vì kĩ thuật kiểm thử này xem xét tính đúng đắn của từng thành phần nhỏ nhất trong mã nguồn. Để giảm thiểu bài toán chi phí, quy trình kiểm thử đơn vị nên được tự động hóa hoàn toàn. Bởi thế, luận văn hướng đến xây dựng một giải pháp kiểm thử tự động mức đơn vị cho các dự án C/C++.
Tư tưởng chính của phương pháp đề xuất dựa trên kĩ thuật kiểm thử tự động định hướng. Hiện nay, kĩ thuật kiểm thử tự động định hướng đã được chứng minh tính hiệu quả trong bài toán kiểm thử tự động. Tuy vậy, các vấn đề còn tồn tại cần giải quyết của kĩ thuật kiểm thử tự động định hướng gồm vấn đề sinh dữ liệu kiểm thử đầu tiên chưa đủ tốt, sinh tập dữ liệu kiểm thử có số lượng nhỏ nhưng đạt độ phủ cao. Do đó, luận văn tập trung giải quyết các bài toán này.
Cụ thể, luận văn đề xuất kĩ thuật sinh dữ liệu kiểm thử đầu tiên dựa trên thông tin phân tích mã nguồn thay vì áp dụng kĩ thuật sinh ngẫu nhiên truyền thống trong kĩ thuật kiểm thử tự động định hướng. Để giảm thiểu số lượng bộ dữ liệu kiểm thử trong khi vẫn đạt độ phủ cao, thuật toán LDFS được đề xuất. Để chứng minh tính hiệu quả của phương pháp đề xuất, công cụ CFT4Cpp được xây dựng dựa trên phương pháp đề xuất và tiến hành so sánh với các phương pháp kiểm thử khác gồm KLEE, PathCrawler, CAUT, CREST. Kết quả nghiên cứu đã được đăng trong hai hội nghị NICS 2016 và SoICT 2017 với đánh giá khả quan về tính thực tiễn của phương pháp đề xuất.
LUAN VAN CHAT LUONG download : add luanvanchat@agmail.com 1 GIỚI THIỆU Kiểm thử đơn vị là một trong những pha quan trọng nhất để đảm bảo chất lượng của phần mềm, đặc biệt các phần mềm nhúng. Hai phương pháp được sử dụng phổ biến gồm kiểm thử hộp đen và kiểm thử hộp trắng.