Tổng quan về phương pháp sinh dữ liệu kiểm thử tự động từ mã nguồn

3TẠP CHÍ KHOA HỌC QUẢN LÝ VÀ CÔNG NGHỆ TỔNG QUAN VỀ PHƯƠNG PHÁP SINH DỮ LIỆU KIỂM THỬ TỰ ĐỘNG TỪ MÃ NGUỒN Trần Nguyên Hương Trường Cao đẳng Sư phạm Trung ương Email: huongtw@gmail.com Tóm tắt: Kiểm thử là quá trình kiểm tra chương trình với mục đích phát hiện lỗi. Kiểm thử phần mềm cần nhiều thời gian và chi phí của dự án, thông thường chiếm 50% chi phí của dự án và 35% tổng thời gian phát triển phần mềm. Bước quan trọng của kiểm thử phần mềm là tự động sinh các bộ dữ liệu kiểm thử từ mã nguồn một cách tối ưu dựa trên các tiêu chuẩn cho trước. Bài báo này tóm tắt các kỹ thuật chính trong việc sinh dữ liệu kiểm thử tự động từ mã nguồn và một số hướng nghiên cứu cải tiến. Từ khóa: Kiểm thử phần mềm, sinh dữ liệu kiểm thử tự động, kiểm thử tĩnh, kiểm thử động, mã nguồn. Vũ Mạnh Điệp Trường Cao đẳng Sư phạm Trung ương Email: diepvm@gmail.com I. TỔNG QUAN VỀ SINH DỮ LIỆU KIỂM THỬ DỰA TRÊN MÃ NGUỒN Trong quá trình phát triển phần mềm, kiểm thử là một giai đoạn quan trọng và thực sự cần thiết để tạo ra phần mềm có chất lượng cao. Có nhiều mức kiểm thử trong giai đoạn này, bao gồm kiểm thử đơn vị, kiểm thử tích hợp, kiểm thử hệ thống và kiểm thử chấp nhận. Trong các mức trên thì kiểm thử đơn vị (unit test) 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. Hai phương pháp được sử dụng phổ biến trong kiểm thử đơn vị gồm kiểm thử hộp đen (black-box testing) và kiểm thử hộp trắng (white-box testing). Kiểm thử hộp đen chỉ kiểm tra tính đúng đắn của đầu ra với đầu vào cho trước mà không quan tâm đến mã nguồn chương trình. Ngược lại, phương pháp kiểm thử hộp trắng đánh giá chất lượng mã nguồn bằng cách sử dụng các kĩ thuật phân tích mã nguồn. Do kiểm thử hộp trắng đi sâu vào phân tích mã nguồn nên kĩ thuật này cho phép phát hiện các lỗi tiềm ẩn mà kiểm thử hộp đen không phát hiện được. Tuy nhiên, chi phí kiểm thử hộp trắng lớn hơn rất nhiều so với kiểm thử hộp đen. Đặc biệt, trong các dự án công nghiệp, chi phí kiểm thử hộp trắng có thể chiếm hơn 50% tổng chi phí phát triển phần mềm. Nguyên nhân của tình trạng này là do số lượng hàm cần kiểm thử lên tới hàng nghìn, thậm chí hàng chục nghìn. Kết quả là chi phí để kiểm thử hết những hàm này khá lớn, ảnh hưởng khá nhiều đến tốc độ phát triển dự án. Vì thế, quá trình kiểm thử hộp 4 TẠP CHÍ KHOA HỌC QUẢN LÝ VÀ CÔNG NGHỆ trắng cần được tự động hóa để giải quyết bài toán về chi phí. Hiện nay, đa số quá trình thực hiện tự động hóa đều tập trung vào việc thực thi ca kiểm thử (test case) mà không quan tâm đến việc thiết kế ca kiểm thử (việc phát hiện lỗi phần mềm phụ thuộc chủ yếu vào chất lượng các ca kiểm thử). Hai thành phần chính trong thiết kế ca kiểm thử là thiết kế dữ liệu kiểm thử và kết quả đầu ra mong đợi (expected output). Tuy nhiên, thiết kế các kết quả đầu ra mong đợi là khó khăn, khó tự động hóa. Do vậy trong thiết kế ca kiểm thử người ta quan tâm nhiều đến sinh dữ liệu kiểm thử. Cho đến nay, có hai kĩ thuật chính để sinh dữ liệu kiểm thử là kĩ thuật kiểm thử tĩnh (static testing) và kiểm thử động (dynamic testing). Điểm chung của các kĩ thuật là sử dụng kĩ thuật thực thi tượng trưng (symbolic execution) và sinh dữ liệu kiểm thử qua giải hệ ràng buộc sử dụng kĩ thuật sinh ngẫu nhiên hoặc bộ giải SMT-Solver. Kĩ thuật thực thi tượng trưng, nêu trong do James C. King giới thiệu lần đầu tiên vào năm 1976, sau đó đã có một số cải tiến trong [5][6] và là một kĩ thuật phổ biến để sinh dữ liệu kiểm thử tự động. Trong bài toán sinh dữ liệu kiểm thử, từ đầu vào là đường thi hành, kỹ thuật này sẽ thay thế các giá trị đầu vào cụ thể bằng các giá trị tượng trưng để đại diện cho một miền các mà hành vi chương trình là như nhau. Tư tưởng chính của kỹ thuật kiểm thử tĩnh là sinh dữ liệu kiểm thử bằng phân tích mã nguồn (không thực thi mã nguồn) sử dụng kĩ thuật thực thi tượng trưng. Quy trình thực hiện như sau: (1) mã nguồn được phân tích và chuyển thành đồ thị dòng điều khiển (control flow graph - CFG) theo tiêu chuẩn bao phủ (coverage criteria) cho trước; (2) sinh các đường kiểm thử (test path) bằng cách duyệt đồ dòng điều khiển; (3) sinh ra hệ ràng buộc từ đường kiểm thử; (4) sinh dữ liệu kiểm thử (ngẫu nhiên hoặc sử dụng bộ giải SMT- solver). Các bước (2), (3), (4) được lặp lại cho đến khi đạt tiêu chí độ phủ hoặc đã duyệt hết các đường kiểm thử. Kỹ thuật kiểm thử tĩnh có ưu điểm là tốc độ thực thi nhanh so với kỹ thuật kiểm thử động, số dữ liệu kiểm thử sinh ra ít (đặc biệt là trong trường hợp chương trình có vòng lặp). Tuy nhiên có hạn chế là độ phức tạp cao vì phải phân tích toàn bộ mã nguồn, kỹ thuật này khó áp dụng cho các dự án công nghiệp bởi vì hỗ trợ tất cả mọi cú pháp là điều không thể. Trái ngược với kỹ thuật kiểm thử tĩnh, kỹ thuật kiểm thử động không yêu cầu phải phân tích mọi cú pháp của chương trình để sinh dữ liệu kiểm thử. Để giảm chi phí phân tích mã nguồn mà vẫn đạt độ phủ cao, kỹ thuật kiểm thử động kết hợp quá trình phân tích cú pháp chương trình với trình biên dịch [1] [2] [3] [10]. Bởi thế, kỹ thuật kiểm thử động dễ dàng đạt được độ phủ cao mà không cần phải phân tích chương trình nhiều. Kỹ thuật kiểm thử động gồm hai kĩ thuật kiểm thử được sử dụng phổ biến gồm kĩ thuật EGT (execution generated testing) và kĩ thuật kiểm thử tự động định hướng (concolic testing): Kĩ thuật EGT được áp dụng trong công cụ sinh dữ liệu kiểm thử tự động nổi tiếng KLEE [2] – một công cụ được đánh giá cao bởi tính hiệu quả của nó. Tư tưởng chính của kĩ thuật EGT là vừa chạy chương trình vừa sinh dữ liệu kiểm thử trực tiếp. Chẳng hạn, khi gặp một điều kiện (điểm quyết định trên đồ thị CFG), dữ liệu kiểm thử tương ứng nhánh đúng và nhánh sai của điều kiện này được sinh ra. Tại đây, với mỗi dữ liệu kiểm thử, một tiến trình mới được tạo ra sẽ phân tích chương trình theo nhánh đúng/sai đó. Quá trình sinh dữ liệu kiểm thử chỉ dừng khi một trong ba điều kiện sau thỏa mãn (i) đạt độ phủ tối đa (ii) không còn nhánh đúng/sai nào để phân tích tiếp, (iii) đạt đến giới hạn thời gian cho phép. Nhược điểm chính của kĩ thuật EGT là hiệu suất thấp khi kiểm thử hàm chứa vòng lặp có số lần lặp lớn, hoặc chứa lời gọi đệ quy. Khi đó, số tiến 5TẠP CHÍ KHOA HỌC QUẢN LÝ VÀ CÔNG NGHỆ trình được tạo ra có thể từ hàng trăm tới hàng nghìn. Kĩ thuật này thể hiện tính hiệu quả khi tìm các lỗi tiềm ẩn trong chương trình bởi vì EGT xem xét mọi trường hợp có thể xảy ra. Tuy nhiên, kĩ thuật EGT không phù hợp với bài toán sinh dữ liệu kiểm thử đạt độ phủ tối đa bởi vì chúng ta không cần xem xét hết mọi trường hợp khi sinh dữ liệu kiểm thử. Kĩ thuật kiểm thử tự động định hướng được đề xuất vào năm 2005 và cài đặt trong công cụ DART [3]. Tư tưởng của kĩ thuật kiểm thử tự động định hướng là sinh dữ liệu kiểm thử kế tiếp từ các dữ liệu kiểm thử trước đó. Sau này, kĩ thuật kiểm thử tự động định hướng liên tục được cải tiến trong các công cụ PathCrawler [10], CUTE [4], CAUT [8][9], và CREST [1]. Quy trình kiểm thử tự động định hướng do Koushik Sen cùng các cộng sự đề xuất DART [3] gồm các bước như sau: Bước 1: Chèn các câu lệnh đánh dấu vào hàm cần kiểm thử (instrument function). Các câu lệnh đánh dấu giúp xác định được danh sách câu lệnh được thực thi khi chạy chương trình. Bước 2: Sinh ngẫu nhiên một bộ dữ liệu kiểm thử đầu tiên dựa trên tham số truyền vào hàm (kiểu cơ sở, con trỏ, mảng, dẫn xuất). Bước 3: Thực thi chương trình với dữ liệu kiểm thử vừa tìm được. Nếu không thực thi được (lỗi xảy ra) thì quay lại bước 2 để sinh bộ giá trị khác. Bước 4: Tìm tập các câu lệnh đã được đi qua với dữ liệu kiểm thử ở bước 3 (đường thi hành – test path) để xây dựng được hệ ràng buộc tương ứng. Bước 5: Tính độ phủ đạt được với dữ liệu kiểm thử mới nhất. Nếu độ phủ đạt được tối đa hoặc hết thời gian, quá trình sinh dữ liệu kiểm thử kết thúc. Ngược lại sang bước 6 Bước 6: Phủ định hệ ràng buộc thu được ở bước 4 để sinh các hệ ràng buộc mới có tác dụng sinh các dữ liệu kiểm thử kế tiếp. Nếu không thể sinh hệ phủ định nào khác, thuật toán kết thúc. Bước 7: Giải hệ ràng buộc thu được ở bước 6 để sinh dữ liệu kiểm thử kế tiếp. Nếu không có dữ liệu kiểm thử nào thỏa mãn, quay về bước 6 để tìm hệ ràng buộc phủ định mới sao cho khác hệ ràng buộc hiện tại. Ngược lại, quay lại bước 3 để chạy dữ liệu kiểm thử kế tiếp này. II. NHỮNG HƯỚNG NGHIÊN CỨU HIỆN NAY 2.1. Phân tích chương trình, tiền xử lý mã nguồn Trước khi thực thi chương trình để sinh dữ liệu kiểm thử tự động từ mã nguồn, chương trình cần phải phân tích, tiền xử lý mã nguồn. Tuy nhiên, phân tích đầy đủ mã nguồn cho một ngôn ngữ lập trình là điều rất khó khăn nhất là khi ngôn ngữ lập trình thường xuyên có sự nâng cấp thành phiên bản mới. Hiện nay, các ngôn ngữ lập trình được phân tích nhiều là ngôn ngữ C/C++, Java, C#. Tuy nhiên, việc phân tích mã nguồn chủ yếu tập trung hỗ trợ cú pháp và các kiểu dữ liệu cơ bản, kiểu con trỏ, kiểu mảng, xử lý vòng lặp. Kỹ thuật thường được áp dụng là sử dụng thư viện phân tích mã nguồn, chẳng hạn Eclipse CDT cho C/C++. Đầu vào của Eclipse CDT là mã nguồn, đầu ra là cây cú pháp trừu tượng (Abstract Syntax Tree – AST) ứng với mã nguồn đó. Từ AST, người ta sẽ xây dựng đồ thị CFG làm cơ sở cho việc thực thi các bước tiếp theo của quá trình kiểm thử tự động. Hiện nay đã có một số nghiên cứu quan tâm đến giải quyết tính hướng đối tượng của ngôn ngữ lập trình, chẳng hạn chương trình có tính đa hình động, khuôn hình lớp. Vấn đề phân tích mã nguồn cần tiếp tục cải tiến để có thể hỗ trợ phân tích đầy đủ cho các chương trình C/C++, Java và nhiều 6 TẠP CHÍ KHOA HỌC QUẢN LÝ VÀ CÔNG NGHỆ ngôn ngữ khác. Các vấn đề còn đang được nghiên cứu như vấn đề quản lý bộ nhớ, phân tích các chương trình có tính kế thừa, chồng toán tử, chồng hàm, khuôn hình v.v. Mặt khác, tối ưu hóa quá trình phân tích mã nguồn là một vấn đề mở cần được nghiên cứu. 2.2. Chiến lược tìm đường thi hành Sau khi thực thi bộ dữ liệu kiểm thử, tập hợp các câu lệnh được thực thi sẽ tạo thành đường thi hành (test path). Hiện tại, nhiều công trình nghiên cứu đưa ra nhiều chiến lược chọn đường thi hành khác nhau để sinh dữ liệu kiểm thử kế tiếp càng tăng độ phủ càng tốt như [1], [8], [10]. Theo tư tưởng của kĩ thuật kiểm thử tự động định hướng, bộ dữ liệu kiểm thử kế tiếp được sinh ra từ nhánh/ câu lệnh chưa được đi qua bởi các bộ dữ liệu kiểm thử trước đó. Có hai loại chiến lược tìm đường thi hành chính bao gồm chiến lược truyền thống và dựa trên đồ thị dòng điều khiển (CFG-based). Chiến lược truyền thống được được Patrice Godefroid đề xuất vào năm 2005 và được áp dụng trong công cụ DART. Các kĩ thuật tìm kiếm trong chiến lược truyền thống gồm: tìm kiếm theo chiều sâu (DFS), tìm kiếm theo chiều rộng (BFS) và tìm kiếm ngẫu nhiên. Theo chiến lược này, điều kiện cuối cùng của đường thi hành mới nhất được phủ định để sinh dữ liệu kiểm thử tiếp theo mà không xét đến trạng thái của đồ thị luồng điều khiển. Tuy nhiên, việc phủ định này có thể khiến quá trình sinh dữ liệu kiểm thử bị lặp vô hạn trong trường hợp hàm có vòng lặp. Sau này, các nghiên cứu trong PathCrawler [10] và CUTE [4] giải quyết vấn đề này bằng cách hạn chế số lần lặp tối đa của vòng lặp. Tiếp nối với các nghiên cứu trước đó, số lượng bộ dữ liệu kiểm thử được giảm thiểu hơn nữa bởi các nghiên cứu của nhóm CREST [1], nhóm CAUT [8] [9] do áp dụng chiến lược dựa trên đồ thị dòng điều khiển để chọn nhánh phủ định tốt nhất. Cụ thể là CREST sử dụng thuật toán Dijkstra để tìm đường thi hành ngắn nhất từ các câu lệnh/nhánh đã thăm tới khối lệnh chưa được thăm; CAUT cố gắng tìm đường thi hành tốt nhất từ câu lệnh đã được thăm đến khối lệnh chưa được khám phá. Các tác giả Nguyễn Đức Anh và Phạm Ngọc Hùng đã đề xuất kĩ thuật xếp hạng đường thi hành theo độ ưu tiên trong [7]. Đường thi hành tăng độ phủ càng lớn thì độ ưu tiên càng cao. Mức độ tăng độ phủ được đánh giá qua trạng thái đồ thị dòng điều khiển (CFG). Trong trường hợp hai đường thi hành cùng tăng độ phủ bằng nhau thì đường thi hành ngắn hơn được ưu tiên hơn. Nguyên nhân bởi vì chi phí phân tích mã nguồn khá lớn, những đường thi hành ngắn hơn được ưu tiên hơn các đường thi hành khác để giảm chi phí phân tích mã nguồn. Ngoài các chiến lược ở trên, hai nhóm chiến lược sau đã được nghiên cứu và sử dụng là nhóm chiến lược tìm kiếm heuristic (Heuristic Search Strategy) và nhóm chiến lược loại bỏ dư thừa (Pruning Redundance Strategy). Đây là các nghiên cứu có nhiều kết quả tốt và phù hợp. 2.3. Tối ưu hóa và giải hệ ràng buộc Kích thước của hệ ràng buộc có thể khá lớn, và cấu trúc khá phức tạp làm tăng thời gian giải hệ ràng buộc. Điều đó dẫn đến bài toán tối ưu hệ ràng buộc trước khi sử dụng SMT-Solver để giải hệ ràng buộc đó. + Loại bỏ ràng buộc không liên quan: Trước khi giải hệ ràng buộc cần xem xét để loại bỏ các ràng buộc không liên quan, nhằm tối ưu hóa hệ ràng buộc. Một vài kĩ thuật đơn giản để giảm độ phức tạp ràng buộc như kĩ thuật đơn giản hóa biểu thức (ví dụ: x+0 > 1 đơn giản hóa thành x >1), kĩ thuật suy biến nhanh giá trị biến (ví dụ: x+1=10 đơn giản hóa thành x=9), kĩ thuật loại bỏ hệ ràng buộc hiển nhiên (ví dụ: x<10, x==5 đơn giản hóa thành x==5), v.v. 7TẠP CHÍ KHOA HỌC QUẢN LÝ VÀ CÔNG NGHỆ Một chú ý quan trọng là mỗi đường thi hành chỉ phụ thuộc vào các điều kiện với một số lượng nhỏ các tham biến. Do vậy một cách tối ưu hóa hiệu quả là cố gắng loại bỏ hết các ràng buộc không liên quan đến kết quả của đường thi hành hiện thời. Ví dụ: Xem xét ràng buộc của một đường thi hành hiện thời của thực thi là: (x+y>0)^(z>0)^(y<12)^(z-x=0). Giả sử chúng ta muốn sinh các giá trị đầu vào mới từ giải ràng buộc (x+y>0)^(z>0)& ¬(y<12) trong đó ¬(y<12) là phủ định của nhánh khả thi được xây dựng từ ràng buộc trên. Ta có thể an toàn loại bỏ z vì ràng buộc này không ảnh hưởng đến kết quả của nhánh ¬(y<12). Loại bỏ ràng buộc thừa với tham chiếu con trỏ và mảng đã được trình bày chi tiết trong các tài liệu [4]. + Kỹ thuật giải hệ ràng buộc: Kĩ thuật tối ưu đầu tiên là kĩ thuật giải hệ ràng buộc tăng dần (incremental solving technique) được đề xuất trong CUTE [4], EXE [11], KLEE [2] và CAUT [8]. Tư tưởng chính của kĩ thuật này là chỉ những hệ ràng buộc liên quan đến hệ ràng buộc phủ định cuối cùng được giải. Ví dụ: Xem xét ràng buộc của một đường đi hiện thời của thực thi là: ((x+y5), một bộ dữ liệu thỏa mãn là {x=6, y=3}. Chúng ta có thể nhanh chóng kiểm tra {x=6, y=3} vẫn thỏa điều kiện (x+y5)^(y≥0) bằng cách chỉ cần quan tâm đến điều kiện y≥0. Kĩ thuật tối ưu hệ ràng buộc thứ hai đề xuất bởi Cristian Cadar và cộng sự được gọi là kĩ thuật kiểm tra tính thỏa mãn dựa trên bộ nhớ đệm (cache-based unsatisfiability check). Kĩ thuật này được áp dụng trong EXE and KLEE. Theo như tư tưởng kĩ thuật này, tất cả các hệ ràng buộc đã được giải đều được lưu lại trong bộ nhớ. Tính luận lý của hệ ràng buộc kế tiếp được xác định nhanh qua đánh giá tập các hệ ràng buộc trước đó. Cụ thể, giả sử trong bộ nhớ lưu hai hệ ràng buộc đã được giải gồm A, B. Trong đó, hệ ràng buộc A có nghiệm, hệ ràng buộc B vô nghiệm. Cho hệ ràng buộc C, tính luận lý hệ ràng buộc này được kiểm tra nhanh như sau. Nếu A C thì hệ ràng buộc C có thể có nghiệm, và nghiệm của A có thể là một phần nghiệm trong C. Nếu B C thì hệ ràng buộc C vô nghiệm, tức hệ ràng buộc C không cần đưa vào bộ giải SMT- Solver để tìm nghiệm. Gần đây, Cristian Cadar và cộng sự đã đề xuất kĩ thuật tối ưu hóa ràng buộc cho mảng [12], đó là cách chuyển đổi dựa trên chỉ số (index-based transformation) và chuyển đổi dự trên giá trị (value-based transformation) để giảm sự phức tạp của các ràng buộc mảng. Nghiên cứu này là mở rộng cho công cụ KLEE. + Lựa chọn và kết hợp các bộ giải SMT- Solver: Một trong những thách thức chính của việc thực thi tượng trưng là giải hệ ràng buộc. Mỗi bộ giải đều có điểm mạnh khác nhau và chỉ giải có hiệu quả một số ràng buộc. Chẳng hạn các công cụ EXE, KLEE, Rwset sử dụng STP-Solver (Simple Theorem Prover) [2] [11]; công cụ Pex, CFT4Cpp sử dụng Z3-Solver; công cụ DART, SMART [13], CUTE sử dụng lp_solver; CREST sử dụng Yices-Solver, SAGE sử dụng Disolver, CFT4CUnit sử dụng SmtInterpol v.v. Cristian Cadar và cộng sự đã đưa ra ý tưởng kết hợp các SMT-Solvers để cùng giải hệ ràng buộc nhanh nhất có thể (được gọi là parallel portfolio solver). Mặc dù công cụ SMT- Solver ngày càng phát triển mạnh, tốc độ giải hệ ràng buộc ngày càng nhanh hơn, tuy nhiên hiện nay vẫn gặp phải một số thách thức như SMT-solver chưa hỗ trợ giải các ràng buộc phi tuyến tính, xử lý biểu thức số thực dấu phẩy động và các ràng buộc phức tạp. 2.4. Giảm thời gian biên dịch Chi phí tạo dữ liệu kiểm thử có thể giảm đáng kể dữ liệu bước biên dịch. Khi một dữ liệu kiểm thử mới được tìm ra, nó được thực 8 TẠP CHÍ KHOA HỌC QUẢN LÝ VÀ CÔNG NGHỆ thi trên môi trường thời gian chạy (runtime environment) để thu thập các câu lệnh đã đi qua. Hiện tại, có hai cách phổ biến để thực thi dữ liệu kiểm thử. Dữ liệu kiểm thử được thực hiện có thể được lưu trữ trực tiếp trong bộ thực thi dữ liệu thử (test driver) hoặc trong một tệp ngoài. Trước đây, với các kiểu dẫn xuất, dữ liệu kiểm thử được phân tích để tạo ra một mã nguồn tương ứng nhằm khởi tạo dữ liệu kiểm thử. Nói cách khác, một trình điều khiển kiểm thử mới được tạo ra mỗi khi có một bộ dữ liệu kiểm thử tiếp theo được tạo ra. Tổng thời gian là thời gian thực hiện ba bước: (i) tạo ra một trình điều khiển kiểm thử mới, (ii) biên dịch dự án kiểm thử với trình điều khiển kiểm thử mới, và (iii) thực thi tệp dữ liệu (tệp dữ liệu có thể lớn đặc biệt là trong các dự án công nghiệp). Chỉ DART, CUTE và CREST mới áp dụng một kĩ thuật để tăng tốc thời gian biên dịch dữ liệu thử nghiệm. Ý tưởng chính của kĩ thuật này là lưu trữ tất cả dữ liệu kiểm thử trong một file bên ngoài và một trình điều khiển kiểm thử phân tích file này để nạp các giá trị của dữ liệu kiểm thử khi thực thi [1] [3]. Bằng cách đó, chỉ có một trình điều khiển kiểm thử duy nhất được tạo ra dùng chung để xử lý tất cả dữ liệu kiểm thử thay vì nhiều phiên bản như trong ý tưởng trước đó. Một ưu điểm lớn của chiến lược này là trình điều khiển kiểm thử chung chỉ cần biên dịch một lần. Tuy nhiên, đề xuất của CREST, DART chỉ áp dụng cho các chương trình C với các dữ liệu cơ bản, con trỏ và mảng mà chưa mở rộng sang các kiểu dữ liệu dẫn xuất của C/C++ (ví dụ cấu trúc, lớp) hoặc mở rộng sang chồng toán tử, kế thừa, đa hình của các chương trình C++. 2.5. Kiểm thử tích hợp Kiểm thử tích hợp (compositional testing) đã được đề xuất trong [13][15][16][17][18][14]. Patrice Godefroid và cộng sự đã mở rộng DART để kiểm thử tích hợp bằng cách đề xuất thuật toán SMART (Systematic Modular Automated Random Testing) [13]. Phương pháp này kiểm thử từng hàm riêng biệt sau đó tóm tắt mỗi hàm thành một biểu thức logic mệnh đề với các điều kiện tiên quyết đầu vào và kết quả đầu ra. Tóm tắt của hàm là phép tuyển của các tóm tắt con, trong đó mỗi tóm tắt con là một phép hội của các điều kiện thu thập được trên mỗi đường thi hành. Các tóm tắt hàm này được sử dụng để kiểm thử các hàm mức cao hơn. Từ nghiên cứu mở đầu này, đã có nhiều cải tiến kỹ thuật kiểm thử tích hợp, tiêu biểu là các nghiên cứu sau: Thứ nhất là cải tiến kỹ thuật sinh tóm tắt hàm bằng công thức logic vị từ cấp 1, sau đó sử dụng SMT để giải [15]; Tiếp theo là cải tiến sinh tóm tắt bắt buộc (must sumaries) để kiểm thử tích hợp khi chương trình có sự tiế