Luận án tiến sĩ các kỹ thuật sinh tự động dữ liệu kiểm thử dựa trên các biểu đồ

CÁC KỸ THUẬT SINH TỰ ĐỘNG DỮ LIỆU KIỂM THỬ DỰA TRÊN CÁC BIỂU ĐỒ UML VŨ THỊ ĐÀO Tháng 04 năm 2018 TIEU LUAN MOI download : skknchat@gmail.com LỜI CẢM ƠN Luận án được thực hiện tại Trường Đại học Công nghệ, Đại học Quốc gia Hà Nội, dưới sự hướng dẫn của PGS. Nguyễn Việt Hà. Tôi xin gửi lời cảm ơn chân thành và sâu sắc nhất tới PGS. Nguyễn Việt Hà – 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ệ.

Người thầy tâm huyết đã tận tình hướng dẫn, động viên khích lệ, dành nhiều thời gian quí báu để định hướng cho tôi trong quá trình tham gia khóa học và hoàn thiện luận án. Tôi xin gửi lời cảm ơn chân thành tới lãnh đạo trường Đại học Công nghệ, lãnh đạo Khoa Công nghệ thông tin, cảm ơn các đồng nghiệp đã tạo điều kiện thuận lợi cho tôi trong quá trình làm luận án. Tôi xin gửi lời cảm ơn chân thành tới các thầy, cô trong 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ệ, những người luôn hướng dẫn, định hướng, góp ý cho tôi trong quá trình viết luận án. Cuối cùng, tôi xin gửi lời cảm ơn sâu sắc tới gia đình và bạn bè, những người đã luôn ủng hộ và hỗ trợ tôi về mọi mặt để tôi yên tâm học tập, nghiên cứu, và hoàn thành luận án.

i TIEU LUAN MOI download : skknchat@gmail.com LỜI CAM ĐOAN Tôi xin cam đoan: Bản luận án tốt nghiệp này là công trình nghiên cứu thực sự của cá nhân. Các kết quả được viết chung với các tác giả khác đều được sự đồng ý của các đồng tác giả trước khi đưa vào luận án. Các kết quả nêu trong luận án là trung thực và chưa từng được công bố dưới bất cứ hình thức nào trước khi trình, bảo vệ và công nhận bởi “Hội Đồng đánh giá luận án tốt nghiệp Tiến sĩ Công nghệ Thông Tin”. Một lần nữa, tôi xin khẳng định về sự trung thực của lời cam kết trên.

Tác giả: ii TIEU LUAN MOI download : skknchat@gmail.com MỤC LỤC LỜI CẢM ƠN i LỜI CAM ĐOAN ii MỤC LỤC iii DANH MỤC CÁC THUẬT NGỮ VÀ KÝ HIỆU vii DANH MỤC CÁC BẢNG ix DANH MỤC CÁC HÌNH VẼ xi TÓM TẮT LUẬN ÁN xiii Chương 1 GIỚI THIỆU 1 1.2 Phương pháp và nội dung nghiên cứu .3 Cấu trúc luận án. 6 Chương 2 KIẾN THỨC NỀN TẢNG 7 2.1 Các khái niệm cơ bản .2 Kiểm thử dựa trên mô hình .3 Các biểu đồ UML và ràng buộc OCL .1 Biểu đồ tuần tự UML và các toán tử .2 Các ràng buộc OCL trong các biểu đồ UML .3 Đồ thị dòng điều khiển. 18 iii TIEU LUAN MOI download : skknchat@gmail.4 Các độ bao phủ và độ phân tích đột biến trong kiểm thử .1 Độ bao phủ tương tranh .2 Độ bao phủ trong kiểm thử vòng lặp .3 Độ phân tích đột biến .5 Tổng quan về sinh dữ liệu kiểm thử tự động .1 Sinh dữ liệu kiểm thử trong kiểm thử cấu trúc .2 Sinh dữ liệu kiểm thử trong kiểm thử chức năng .3 Sinh dữ liệu kiểm thử tự động từ các biểu đồ UML .6 Các công cụ sinh dữ liệu kiểm thử hiện tại. 34 Chương 3 SINH DỮ LIỆU KIỂM THỬ CHO KIỂU DỮ LIỆU SỐ VÀ CẤU TRÚC ĐỘNG 35 3.2 Những nghiên cứu liên quan .3 Phương pháp sinh dữ liệu kiểm thử cho biến kiểu dữ liệu số và cấu trúc động .1 Tổng quan về phương pháp đề xuất .2 Chuyển đổi biểu đồ tuần tự UML thành CFG .3 Sinh các kịch bản kiểm thử .4 Chọn các vị từ và chuyển thành các hàm vị từ .5 Hàm vị từ với các ràng buộc OCL .6 Sinh dữ liệu kiểm thử từ các hàm vị từ .2 Kết quả và đánh giá.

85 Chương 4 SINH DỮ LIỆU KIỂM THỬ CHO VÒNG LẶP VÀ iv TIEU LUAN MOI download : skknchat@gmail.com CÁC ỨNG DỤNG TƯƠNG TRANH 87 4.2 Những nghiên cứu liên quan .3 Phương pháp sinh dữ liệu kiểm thử theo các độ bao phủ tương tranh và lặp .1 Tổng quan về phương pháp đề xuất .2 Sinh các kịch bản kiểm thử .3 Sinh dữ liệu kiểm thử .2 Kết quả và đánh giá. 113 Chương 5 SINH DỮ LIỆU KIỂM THỬ CHO KIỂU DỮ LIỆU CHUỖI 115 5.2 Những nghiên cứu liên quan .3 Phương pháp sinh tự động dữ liệu kiểm thử cho các ràng buộc chuỗi .1 Tổng quan về phương pháp đề xuất .2 Sinh các kịch bản kiểm thử .3 Giải các ràng buộc chuỗi .2 Kết quả và đánh giá. 142 Chương 6 KẾT LUẬN 144 6.1 Các kết quả đạt được của luận án. 144 v TIEU LUAN MOI download : skknchat@gmail.2 Hướng nghiên cứu tiếp theo.

146 DANH MỤC CÁC CÔNG TRÌNH KHOA HỌC CỦA TÁC GIẢ LIÊN QUAN ĐẾN LUẬN ÁN 148 TÀI LIỆU THAM KHẢO 149 vi TIEU LUAN MOI download : skknchat@gmail.com DANH MỤC CÁC THUẬT NGỮ VÀ KÝ HIỆU Tên thuật ngữ đầy đủ Chữ viết tắt Giải nghĩa Breadth-first search BFS Thuật toán tìm kiếm theo chiều rộng Black box testing Kiểm thử hộp đen Control Flow Graph CFG Đồ thị dòng điều khiển Constraint solver Bộ giải ràng buộc Coverage criteria Tiêu chuẩn bao phủ Dynamic Domain Reduction DDR Phương pháp giảm miền động Deadlock Khóa chết Depth-first search DFS Thuật toán tìm kiếm theo chiều sâu Extended Finite State Machine EFSM Máy hữu hạn trang thái mở rộng Finite State Machine FSM Máy hữu hạn trạng thái Gray box testing Kiểm thử hộp xám Invariant Bất biến Linear Temporal Logic LTL Logic thời gian tuyến tính Message Thông điệp Model Checking Kiểm chứng mô hình Mutation Score MS Độ đo đột biến Object Constraint Language OCL Ngôn ngữ ràng buộc đối tượng Parallel Fragment Par Toán tử song song Post–condition Hậu điều kiện Pre–condition Tiền điều kiện Predicate Vị từ Safety property Thuộc tính an toàn Satisfiable SAT Thỏa mãn Symbolic execution SE Thực thi tượng trưng Weak Sequencing Fragment Seq Toán tử tuần tự yếu vii TIEU LUAN MOI download : skknchat@gmail.com Tên thuật ngữ đầy đủ Chữ viết tắt Giải nghĩa Satisfiability Modulo Theories SMT Các lý thuyết môđun về tính thỏa được System Under Testing SUT Hệ thống được kiểm thử Test Case Ca kiểm thử Test Data Dữ liệu kiểm thử Test Scenario Kịch bản kiểm thử Test Script Mã kiểm thử dạng đặc tả kịch bản dùng để tự động hóa Unified Modeling Language UML Ngôn ngữ mô hình hóa thống nhất Unsatisfiable UNSAT Không thỏa mãn Variable Assignment Graph VAG Đồ thị tham số biến White box testing Kiểm thử hộp trắng eXtensible Markup Language XML Ngôn ngữ đánh dấu mở rộng Z3-Str solver Bộ giải Z3-Str viii TIEU LUAN MOI download : skknchat@gmail.com DANH MỤC CÁC BẢNG 2.1 Các biểu đồ UML và sử dụng để mô hình hóa cho kiểm thử [100] 30 3.1 Bảng giá trị chân lý cho các toán tử logic [3] .2 Hàm vị từ cho các toán tử logic trong OCL [3] .3 Hàm vị từ cho các toán tử quan hệ OCL cho kiểu dữ liệu số [3] .4 Các kịch bản kiểm thử được sinh ra của máy bán hàng tự động .5 So sánh kết quả đề xuất và kết quả nghiên cứu trong [72] .6 Thực nghiệm đưa ra độ bao phủ các đường dẫn của đồ thị của phương pháp đưa ra và phương pháp kiểm thử ngẫu nhiên .7 Kết quả thực nghiệm so sánh phương pháp đề xuất với phương pháp [30] .1 Kết quả MS sử dụng cho từng kịch bản kiểm thử được sinh ra trong cách tiếp cận [95] và Phương pháp đề xuất .2 Kết quả MS của phương pháp đề xuất và phương pháp ngẫu nhiên112 5.1 Ví dụ giải các toán tử chuỗi .2 Cách Z3–str thực hiện xử lý các ràng buộc chuỗi trong Bảng 5.3 Ngữ pháp của các ràng buộc trong Z3–str, mở rộng cho search và replaceAll so với [114] .4 Định nghĩa cho Thuật toán 5.5 Các quy tắc giảm [114] .6 Quy tắc giảm sử dụng gọi đệ quy .7 Các quy tắc tiền xử lý cho các toán tử chuỗi .8 So sánh khả năng tìm lỗi của các chức năng trong các ứng dụng. 140 ix TIEU LUAN MOI download : skknchat@gmail.9 So sánh xử lý các toán tử chuỗi và hiệu năng của SeqString với phương pháp của nhóm Tác giả Shoichiro [39] .624801 TIEU LUAN MOI download : skknchat@gmail.624801 DANH MỤC CÁC HÌNH VẼ 1.1 Các nội dung luận án giải quyết trong bài toán kiểm thử dựa trên mô hình.1 Quy trình kiểm thử dựa trên mô hình [100].2 Ví dụ biểu đồ tuần tự UML có toán tử alt và opt.3 Ví dụ biểu đồ tuần tự UML có toán tử loop và break.4 Ví dụ biểu đồ tuần tự UML có toán tử par và seq.5 Ví dụ biểu đồ tuần tự UML có toán tử strict và critical.6 Ví dụ biểu đồ tuần tự UML có toán tử ignore và consider.7 Ví dụ biểu đồ tuần tự UML có toán tử negative và assert.8 Ví dụ biểu đồ lớp.9 Các loại nút của đồ thị dòng điều khiển .10 Các hướng tiếp cận của sinh dữ liệu kiểm thử tự động [99].11 Phân loại các công cụ sinh kiểm thử tự động [40].1 Sinh ca kiểm thử sử dụng kiểm chứng mô hình theo cách tiếp cận [17].2 Các bước cơ bản sinh các dữ liệu kiểm thử.3 Ví dụ biểu đồ tuần tự UML.4 File xmi sau khi chuẩn hóa mô tả dữ liệu của biểu đồ tuần tự trong Hình 3.5 Chuyển từ biểu đồ tuần tự sang CFG (của toán tử opt và alt).6 Chuyển từ biểu đồ tuần tự sang CFG (của toán tử break và loop).7 Chuyển từ biểu đồ tuần tự sang CFG (của toán tử par và seq).8 Chuyển từ biểu đồ tuần tự sang CFG (của toán tử strict và critical).624801 TIEU LUAN MOI download : skknchat@gmail.9 Chuyển từ biểu đồ tuần tự sang CFG (của toán tử ignore và consider).10 Chuyển từ biểu đồ tuần tự sang CFG (của toán tử assert và negative).11 Biểu đồ tuần tự của máy bán hàng tự động.12 Biểu đồ lớp của chức năng máy bán hàng tự động.13 Đồ thị dòng điều khiển của máy bán hàng tự động.14 Biểu đồ tuần tự với kiểu dữ liệu biến là cấu trúc động.15 Đồ thị dòng điều khiển với kiểu dữ liệu biến là cấu trúc động.16 Đường dẫn con P1 thực thi.17 Đường dẫn con P2 thực thi.18 Đường dẫn con P3 thực thi.19 Kiến trúc thực thi của SequenceTesting.1 Toán tử lặp chuyển sang CFG.2 Toán tử song song chuyển sang CFG.3 Quá trình sinh dữ liệu kiểm thử: phát triển từ [75] cho vòng lặp.4 Tính điểm chia split phụ thuộc các miền giá trị của biến trong [75].5 Biểu đồ tuần tự của chức năng chuyển tiền trong hệ thống ngân hàng.6 Biểu đồ lớp và ràng buộc OCL cho chức năng chuyển tiền.7 Đồ thị dòng điều khiển của chức năng chuyển tiền.8 Kiến trúc phát triển của công cụ SequenceConcur.1 Kiến trúc của Bộ giải Z3–str trong [114].2 Biểu đồ tuần tự cho chức năng kiểm tra thông tin của một ứng dụng web.