Tổng quan luận án

Hoạt động kiểm thử phần mềm (software testing) là một khâu trọng yếu trong chu trình phát triển phần mềm, chiếm khoảng 50% đến 60% tổng chi phí toàn bộ quy trình. Việc thiết kế và chuẩn bị bộ dữ liệu kiểm thử (test case) thủ công đòi hỏi nguồn nhân lực lớn nhưng khó đảm bảo tính bao phủ đầy đủ trên toàn bộ các đường tính toán của chương trình. Nhằm giảm thiểu chi phí và nâng cao độ tin cậy, các phương pháp tự động sinh ca kiểm thử dựa trên mã nguồn đang được tập trung nghiên cứu. Trong các kỹ thuật hiện nay, thực thi biểu trưng (symbolic execution) cho thấy tiềm năng lớn trong việc phát hiện lỗi và phân tích đường thực thi. Tuy nhiên, kỹ thuật này gặp phải những trở ngại kỹ thuật lớn, đặc biệt là hiện tượng bùng nổ đường đi và sự phức tạp khi xử lý các ràng buộc trên kiểu dữ liệu xâu ký tự và dữ liệu hỗn hợp. Luận án lựa chọn giải quyết khoảng trống nghiên cứu về cải tiến mô hình hóa và nâng cao hiệu năng của bộ giải ràng buộc xâu áp dụng trong tự động sinh ca kiểm thử cho các chương trình Java.

Mục tiêu nghiên cứu của luận án được xác định cụ thể bao gồm:

  1. Nghiên cứu các phương pháp mô hình hóa ràng buộc và giải ràng buộc, từ đó cải tiến khả năng giải ràng buộc và áp dụng kỹ thuật thực thi biểu trưng trong tự động sinh các ca kiểm thử.
  2. Cài đặt thử nghiệm các phương pháp đề xuất trong sinh tự động các ca kiểm thử trên kiểu dữ liệu xâu và kiểu dữ liệu hỗn hợp.
  3. Phân tích, đánh giá kết quả sau khi thử nghiệm.

Đối tượng và phạm vi nghiên cứu của luận án:

  • Đối tượng nghiên cứu: Các phương pháp tự động sinh ca kiểm thử phần mềm; kỹ thuật thực thi biểu trưng tĩnh và động; các kỹ thuật mô hình hóa ràng buộc và giải ràng buộc trên các kiểu dữ liệu khác nhau, đặc biệt là kiểu dữ liệu xâu và dữ liệu hỗn hợp.
  • Phạm vi nghiên cứu: Tập trung vào các kỹ thuật giải ràng buộc xâu dựa trên hai phương pháp chính là Otomat (Automata) và Bitvector; môi trường thực nghiệm và đánh giá được triển khai trên ngôn ngữ Java, khai thác các thư viện xử lý xâu ký tự và công cụ kiểm chứng mô hình Java PathFinder (JPF).

Tổng quan tài liệu và vị trí của luận án

Trong bức tranh tổng quan về kiểm thử tự động, luận án điểm lại hai hướng tiếp cận căn bản: sinh dữ liệu kiểm thử dựa vào mô hình (model-based) và sinh dữ liệu kiểm thử dựa vào mã nguồn (code-based) [1-7]. Các kỹ thuật sinh dữ liệu kiểm thử tự động đã được công bố bao gồm:

  • Kỹ thuật dựa vào chứng minh định lý (theorem proving) [8, 9].
  • Kỹ thuật dựa vào thực thi biểu trưng (symbolic execution) [5, 7, 10-12].
  • Kỹ thuật dựa vào kiểm chứng mô hình (model checking) [13, 16].
  • Kỹ thuật dựa vào mô hình luồng sự kiện (event-flow model) [14].
  • Kỹ thuật dựa vào mô hình xích Markov (Markov chains model) [15].

Lịch sử phát triển của kỹ thuật thực thi biểu trưng bắt đầu từ các nghiên cứu nền tảng năm 1976 của Lori Clarke và James King [31], sau đó được mở rộng sang giai đoạn thực thi biểu trưng thực tế từ năm 2005 đến nay. Hướng tiếp cận này được triển khai trên nhiều công cụ và ngôn ngữ như DART [36], CUTE [35], CREST cho C/C++; PEX [36, 37] cho .NET; KLEE [30], Cloud9, Otter [12], SAGE [63], EXE [17, 55], Austin [58] và Java PathFinder (JPF) [68] cho Java.

Để giải quyết thách thức bùng nổ đường đi trong thực thi biểu trưng, các công trình trước đây tập trung vào:

  • Kỹ thuật tìm kiếm kinh nghiệm (heuristic): Tìm kiếm đường dẫn ngẫu nhiên, tìm kiếm theo đồ thị luồng điều khiển, ưu tiên câu lệnh có số lần chạy ít nhất [17, 55], kết hợp tìm kiếm tiến hóa [30, 56-58] hoặc kiểm thử đột biến [59].
  • Kỹ thuật phân tích tính đúng đắn của chương trình: Gộp đường dẫn theo hướng tĩnh [35], sử dụng bộ nhớ đệm và tóm tắt hàm (function summarization) [58, 59], cắt tỉa đường dẫn tương đương [66, 67], và sinh ca kiểm thử lười [62].
  • Xử lý tương tác môi trường: Gọi trực tiếp, mô hình hóa cuộc gọi hệ thống trong kernel/thư viện (như KLEE, Cloud9, Otter), hoặc phân nhánh toàn bộ trạng thái máy ảo [12, 30].

Đối với bài toán giải ràng buộc xâu (String Constraint Solving), từ năm 2010 đã có nhiều nghiên cứu ứng dụng trong phân tích phần mềm, kiểm chứng mô hình, cơ sở dữ liệu và an ninh web [47-52]. Các tiếp cận chính bao gồm: tiếp cận dựa trên Otomat hữu hạn, tiếp cận dựa trên từ sử dụng lý thuyết thỏa mãn modulo (SMT) [53], và tiếp cận phân tách xâu thành số nguyên hoặc bitvector qua các bộ giải như STP [35] hay Z3 [64].

Khoảng trống luận án lựa chọn giải quyết: Mặc dù kỹ thuật thực thi biểu trưng đã được tích hợp trong các công cụ phân tích, hiệu năng thực tế khi xử lý các ràng buộc phức tạp trên kiểu dữ liệu xâu và dữ liệu hỗn hợp trong môi trường Java vẫn còn hạn chế về mặt thời gian thực thi. Luận án tập trung xây dựng mô hình hóa ràng buộc xâu, cải tiến thuật toán giải ràng buộc kết hợp giữa Otomat và Bitvector, từ đó tối ưu hóa quá trình sinh ca kiểm thử tự động trên nền tảng Java.

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

Luận án xây dựng trên các nền tảng lý thuyết và phương pháp sau:

  • Khung lý thuyết kiểm thử và mô hình phát triển: Vòng đời phát triển phần mềm (SDLC) kết hợp vòng đời kiểm thử phần mềm (STLC) theo mô hình chữ V (V-model) và mô hình phát triển lặp; các tiêu chuẩn bao phủ dòng điều khiển gồm phủ câu lệnh (statement coverage), phủ rẽ nhánh (branch coverage) và phủ điều kiện con (condition coverage).
  • Lý thuyết thực thi biểu trưng và thực thi Concolic: Mô hình hóa chương trình $P$ như một hàm chuyển đổi trạng thái $P: S \to R$ với vector đầu vào $I = (x_1, \dots, x_n)$; biểu diễn cấu trúc qua đồ thị dòng điều khiển (CFG) $G = (N, E, s, e)$ với các khối cơ bản (basic blocks); xây dựng cây thực thi biểu trưng (SET) và điều kiện đường đi (Path Condition - PC) tích lũy qua các điểm rẽ nhánh.
  • Lý thuyết ngôn ngữ hình thức và ràng buộc xâu: Định nghĩa bảng chữ cái hữu hạn $\Sigma$, tập xâu $\Sigma^*$, xâu rỗng $\varepsilon$, độ dài $|w|$, phép nối $v.w$, phép lặp $w^n$, và ngôn ngữ $L(M)$ đoán nhận bởi Otomat hữu hạn $M$. Phân loại biến xâu theo 3 cấp độ: không giới hạn độ dài, có giới hạn độ dài ($\lambda$), và cố định độ dài ($\lambda$).
Phép toán ràng buộc xâu Ký hiệu toán học / logic Diễn giải ngữ nghĩa
So sánh bằng / khác $x = y, x \neq y$ So sánh tính tương đương giữa hai biến xâu
So sánh thứ tự logic $x < y, x \le y, x \ge y, x > y$ Quan hệ thứ tự từ điển giữa hai xâu
Độ dài xâu $n = |x|$ Ràng buộc độ dài của xâu $x$ bằng số nguyên $n$
Phép nối và lặp $z = x.y, y = x^n$ Nối hai xâu hoặc lặp lại $n$ lần phép nối xâu $x$
Đảo ngược xâu $y = x^{-1}$ Đảo ngược thứ tự các ký tự trong xâu
Cắt xâu con $y = x[i..j]$ Trích xuất xâu con từ chỉ số $i$ đến $j$ của xâu $x$
Tìm kiếm vị trí $n = find(x, y)$ Chỉ số xuất hiện đầu tiên của xâu $x$ trong xâu $y$
Thay thế xâu $y = replace(x, q, q')$ Thay thế lần xuất hiện đầu tiên của $q$ bằng $q'$ trong $x$
  • Phương pháp thực nghiệm và công cụ:
    • Phương pháp sửa đổi mã nguồn (instrumentation): Sử dụng ngôn ngữ trung gian Jimple và bộ khung Soot framework [40] để chuyển đổi và chèn mã vào Java bytecode; ứng dụng kỹ thuật phân tích con trỏ tĩnh bảo thủ [43-46] và kỹ thuật phân tích dựa trên kiểu [41]. Khai thác mã nguồn mở của Java qua dự án OpenJDK [42].
    • Cấu trúc lưu trữ trạng thái biểu trưng: Cài đặt các bảng ánh xạ dạng Map ($key \to value$) gồm ánh xạ biến cơ sở $S$, ánh xạ đối tượng $R$, và ánh xạ bộ nhớ $M$; áp dụng cơ chế khởi tạo lười (lazy initialization) khi xử lý tham số đầu vào là đối tượng tham chiếu.
    • Môi trường kiểm chứng mô hình: Sử dụng công cụ Java PathFinder (JPF) [68] với kiến trúc phân tầng gồm hai thành phần cốt lõi là máy ảo JVM (bộ sinh trạng thái Java bytecode) và bộ tìm kiếm Search (điều hướng và đánh giá không gian trạng thái).

Nội dung chính theo từng chương

Chương 1: Tổng quan về kiểm thử phần mềm và thực thi biểu trưng

Chương 1 hệ thống hóa cơ sở lý thuyết về kiểm thử phần mềm và kỹ thuật thực thi biểu trưng ứng dụng trong tự động sinh ca kiểm thử.

  • Khái niệm và quy trình kiểm thử: Trình bày vai trò của kiểm thử trong tiến trình bảo đảm chất lượng phần mềm (SQA), các khái niệm kế hoạch kiểm thử (test plan) và ca kiểm thử (gồm bộ ba: tập dữ liệu đầu vào, trạng thái thành phần phần mềm, tập kết quả kỳ vọng). Phân tích các tiêu chuẩn dừng kiểm thử dựa trên tiêu tốn tài nguyên hoặc hoàn thành kế hoạch, kết hợp tiêu chuẩn thống kê hướng sử dụng và tiêu chuẩn hướng bao phủ.
  • Phân loại và kỹ thuật kiểm thử: Phân biệt kiểm thử hộp đen, kiểm thử hộp trắng; các mức độ kiểm thử từ kiểm thử đơn vị (unit test), kiểm thử tích hợp (integration test), kiểm thử hệ thống (system test) đến kiểm thử chấp nhận (gồm kiểm thử Alpha và Beta); các hình thức kiểm thử chức năng, phi chức năng, kiểm thử cấu hình (shakeout test, smoke test), hiệu suất và hồi quy.
  • Kiểm thử dòng điều khiển tĩnh và động: Trình bày quy trình kiểm thử động 6 bước (chèn mã bằng công cụ DMS/SRT với các luật rule... rewrite to, khởi tạo ca kiểm thử, thực thi, tái tạo hệ ràng buộc, phủ định hệ ràng buộc, và giải hệ ràng buộc mới). So sánh với quy trình kiểm thử tĩnh dựa trên đồ thị dòng điều khiển (CFG).
Tiêu chí so sánh Kiểm thử dòng điều khiển theo hướng tĩnh Kiểm thử dòng điều khiển theo hướng động
Môi trường thực thi Mã nguồn không thực thi lặp lại trong môi trường chạy; chỉ chạy 1 lần để xác minh ca kiểm thử Mã nguồn được chèn thêm khối lệnh và thực thi lặp lại nhiều lần
Cơ chế phân tích Xây dựng đồ thị dòng điều khiển (CFG), trích xuất tập đường kiểm thử độc lập Thực thi cụ thể, thu thập ràng buộc thực tế, phủ định ràng buộc tại điểm rẽ nhánh
Xử lý vòng lặp xác định số lần lặp tối đa Tái cấu trúc đường đi, sinh ra cố định 7 đường kiểm thử mới Sử dụng kỹ thuật phủ định hệ, số ca kiểm thử phụ thuộc vào độ sâu thực thi
Xử lý vòng lặp không xác định số lần lặp Sinh ra cố định 4 đường kiểm thử mới Dễ dẫn đến số ca kiểm thử không xác định hoặc bùng nổ đường đi (ví dụ: while (m!=n))
Công cụ hỗ trợ tiêu biểu Các bộ phân tích đồ thị luồng điều khiển và bộ giải ràng buộc tĩnh Công cụ chèn mã DMS/SRT, PathCrawler, DART, CUTE
  • Cấu trúc đồ thị dòng điều khiển (CFG): Định nghĩa 5 loại đỉnh gồm đỉnh xuất phát, đỉnh kết thúc, đỉnh quyết định (câu lệnh điều kiện rẽ nhánh), đỉnh kết nối (nơi hội tụ của nhiều luồng điều khiển), và đỉnh xử lý (câu lệnh gán, khai báo, khởi tạo). Định nghĩa tập đường đi độc lập và đường kiểm thử.
  • Kỹ thuật thực thi biểu trưng tĩnh và động (DSE): Trình bày cơ chế thay thế giá trị cụ thể bằng ký hiệu biểu trưng ($\lambda$), cập nhật điều kiện đường đi (PC) tại các câu lệnh rẽ nhánh và xây dựng cây thực thi biểu trưng (SET). Trình bày thuật toán DSE qua 6 bước (từ Bước 0 khởi tạo tập đã thực thi $J := \emptyset$, duyệt chọn đầu vào $i \notin J$, thực thi $P(i)$, thu thập ràng buộc $C(i)$, suy ra ràng buộc phủ định $C'(i)$, đến giải ràng buộc $Solve(C'(i))$ để cập nhật $J$). Minh họa cơ chế khởi tạo lười cho đối tượng tham chiếu (SimpleList), quản lý ánh xạ biểu trưng $S(x)$ và $R(o)$, cơ chế ngăn xếp lưu trữ giá trị trả về trong các lời gọi phương thức, và kỹ thuật tạo trạng thái chụp nhanh (snapshot state) kết hợp phân tích con trỏ tĩnh bảo thủ để bỏ qua các hàm không liên quan.
  • Lý thuyết ràng buộc xâu: Trình bày hệ thống ký hiệu hình thức cho biến xâu, các phép toán trên xâu, và 3 hướng tiếp cận giải ràng buộc xâu (dựa trên Otomat, dựa trên từ/SMT, và dựa trên phân tách xâu/Bitvector).

Chương 2: Thực thi biểu trưng và mô hình hóa ràng buộc

Chương 2 phân tích các khó khăn nội tại của thực thi biểu trưng, giới thiệu các công cụ mở rộng và trình bày các phương pháp mô hình hóa ràng buộc. Nội dung chương phản ánh các kết quả nghiên cứu đã công bố của tác giả trong các công trình [CT1], [CT2], [CT3], [CT5].

  • Phân tích thách thức bùng nổ đường đi: Đánh giá hiện tượng số lượng đường thực thi tăng theo hàm mũ của các câu lệnh rẽ nhánh tĩnh. Tổng hợp các giải pháp khắc phục:
    • Tìm kiếm kinh nghiệm (heuristic): Điều hướng dựa trên đồ thị dòng điều khiển, ưu tiên câu lệnh có tần suất thực thi ít nhất (như trong công cụ EXE), khám phá ngẫu nhiên, hoặc tích hợp thuật toán tìm kiếm tiến hóa với hàm mục tiêu định hướng không gian đầu vào (công cụ Austin [58]).
    • Kỹ thuật phân tích tính đúng đắn: Phương pháp gộp đường dẫn tĩnh [35], kỹ thuật sử dụng bộ nhớ đệm và tóm tắt hàm [58, 59], và kỹ thuật sinh ca kiểm thử lười [62] nhằm tự động cắt tỉa các đường dẫn dư thừa có cùng trạng thái và ràng buộc.
  • Mô hình hóa bộ nhớ: Phân tích sự đánh đổi giữa độ chính xác và khả năng mở rộng khi mô hình hóa các kiểu dữ liệu nguyên (integer overflow), con trỏ và mảng ($A[i]$) thông qua các bộ giải STP [35], Z3 [64] trong các công cụ KLEE, SAGE, DART, CUTE, CREST.
  • Môi trường kiểm chứng Java PathFinder (JPF):
    • Phân tích kiến trúc mức cao của JPF: Cấu trúc gồm hai khối chức năng chính là Java Virtual Machine (JVM) chuyên thực thi chỉ thị Java bytecode để tạo trạng thái cụ thể, và Search Driver chịu trách nhiệm điều hướng duyệt không gian trạng thái, kích hoạt quay lui và kiểm tra vi phạm thuộc tính.
    • Năng lực phát hiện lỗi: Minh họa cơ chế kiểm chứng của JPF qua ví dụ lớp Rand.java với hai biến ngẫu nhiên $a \in [0, 2]$, $b \in [0, 3]$ và biểu thức $c = a / (b + a - 2)$. Trong khi thực thi thông thường chỉ thu được một kết quả ngẫu nhiên đơn lẻ, JPF duyệt toàn bộ không gian trạng thái của chương trình và phát hiện được 2 trường hợp lỗi ngoại lệ do phép chia cho 0.

Chương 3: Cải tiến mô hình hóa và giải ràng buộc trên kiểu xâu và dữ liệu hỗn hợp

Chương 3 trình bày các đề xuất cải tiến của luận án đối với bài toán mô hình hóa và giải ràng buộc xâu:

  • Xây dựng mô hình hóa ràng buộc trên kiểu dữ liệu xâu ký tự và các hệ ràng buộc hỗn hợp (kết hợp giữa biến kiểu xâu, kiểu số nguyên đại diện cho độ dài/vị trí, và các kiểu dữ liệu cơ sở khác).
  • Cải tiến kỹ thuật giải ràng buộc trong thực thi biểu trưng dựa trên sự kết hợp giữa phương pháp Otomat hữu hạn và kỹ thuật phân tách xâu Bitvector.
  • Mở rộng kỹ thuật thực thi biểu trưng và phát triển mô-đun giải ràng buộc tích hợp vào công cụ Java PathFinder (JPF), tối ưu hóa các biểu thức ràng buộc đường dẫn nhằm giảm thời gian thực thi mà vẫn duy trì độ bao phủ kiểm thử theo các tiêu chí đã định.

Kết quả và những đóng góp mới

Các đóng góp mới về mặt lý luận và thực tiễn được luận án xác định bao gồm:

  1. Đóng góp về lý luận và mô hình: Xây dựng phương pháp mô hình hóa ràng buộc trên kiểu dữ liệu xâu và hệ ràng buộc hỗn hợp; đề xuất giải pháp cải tiến khả năng giải ràng buộc đường dẫn trong kỹ thuật thực thi biểu trưng.
  2. Đóng góp về kỹ thuật và thuật toán: Cài đặt kỹ thuật mô hình hóa và giải ràng buộc kết hợp giữa Otomat và Bitvector phục vụ giải quyết các biểu thức ràng buộc xâu phức tạp.
  3. Đóng góp về công cụ và thực nghiệm: Mở rộng nền tảng kiểm chứng Java PathFinder (JPF), áp dụng thuật toán tối ưu hóa ràng buộc lộ trình thực thi trên các chương trình Java thực nghiệm, giúp giảm thời gian thực thi của bộ công cụ trong khi vẫn đảm bảo độ bao phủ mã nguồn.

Hạn chế và hướng nghiên cứu tiếp

Hạn chế của nghiên cứu:

  • Hiện tượng bùng nổ đường đi vẫn là rào cản khi mở rộng kỹ thuật sang các chương trình có kích thước lớn hoặc chứa các cấu trúc vòng lặp không xác định được số lần lặp tối đa.
  • Xử lý địa chỉ biểu trưng và con trỏ phức tạp: Khi các biến biểu trưng trỏ tới nhiều vị trí bộ nhớ khác nhau, việc khôi phục trạng thái từ các hàm bị bỏ qua gặp khó khăn và có thể dẫn đến bùng nổ đường dẫn.
  • Xử lý các lời gọi phương thức thư viện chuẩn và tương tác môi trường: Phương pháp chèn mã trung gian (Jimple/Soot) phụ thuộc vào tính sẵn có của mã nguồn; việc mô hình hóa các cuộc gọi hệ thống hoặc các phương thức native chưa có mã nguồn đòi hỏi chi phí bảo trì và xây dựng mô hình giả lập phức tạp.

Hướng nghiên cứu tiếp:

  • Tiếp tục hoàn thiện và tối ưu hóa thuật toán giải ràng buộc xâu trên các hệ ràng buộc hỗn hợp có độ phức tạp cao hơn.
  • Mở rộng cơ chế mô hình hóa môi trường và thư viện ngoài cho Java PathFinder nhằm hỗ trợ đầy đủ các API chuẩn của Java mà không cần sửa đổi mã nguồn thủ công.
  • Nghiên cứu kết hợp sâu hơn giữa thực thi biểu trưng động với các kỹ thuật học máy hoặc tìm kiếm tiến hóa nâng cao để tối ưu hóa việc định hướng không gian dữ liệu đầu vào trên các hệ thống phần mềm quy mô công nghiệp.

Giá trị tham khảo

Nội dung luận án mang lại giá trị tham khảo cho các nhóm đối tượng:

  • Nghiên cứu sinh và học viên cao học ngành Khoa học máy tính, Kỹ nghệ phần mềm: Có thể tham khảo hệ thống lý thuyết về kiểm thử dòng điều khiển, các tiêu chí phủ, nguyên lý thực thi biểu trưng tĩnh/động, thuật toán DSE, và các mô hình biểu diễn ràng buộc xâu hình thức.
  • Giảng viên và nhà nghiên cứu trong lĩnh vực kiểm chứng phần mềm: Sử dụng các tài liệu phân tích về cơ chế khởi tạo lười, chuyển đổi ngôn ngữ trung gian Jimple qua Soot framework, và kiến trúc hoạt động của Java PathFinder (JPF) để phục vụ công tác giảng dạy và nghiên cứu chuyên sâu.
  • Kỹ sư phát triển công cụ kiểm thử tự động (Testing Tool Developers): Tham khảo giải pháp kết hợp giữa Otomat và Bitvector để xây dựng các bộ giải ràng buộc chuyên dụng cho ngôn ngữ Java, cũng như phương pháp chèn mã và thu thập điều kiện đường đi phục vụ sinh dữ liệu kiểm thử đơn vị tự động.

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

  1. Kỹ thuật thực thi biểu trưng giải quyết bài toán sinh ca kiểm thử tự động theo nguyên lý nào?
    Thực thi biểu trưng gán các ký hiệu biểu trưng đại diện cho miền giá trị đầu vào thay vì sử dụng giá trị cụ thể. Khi duyệt qua các câu lệnh rẽ nhánh trong mã nguồn, công cụ thu thập các biểu thức điều kiện (hoặc phủ định của chúng) để tích lũy thành điều kiện đường đi (Path Condition - PC). Bộ giải ràng buộc sau đó xử lý các biểu thức logic trong PC để tìm ra bộ giá trị đầu vào cụ thể thỏa mãn, giúp chương trình thực thi chính xác theo đường dẫn mong muốn.

  2. Sự khác biệt cốt lõi giữa kiểm thử dòng điều khiển theo hướng tĩnh và hướng động khi xử lý vòng lặp là gì?
    Trong kiểm thử tĩnh, các đường kiểm thử chứa vòng lặp được tái cấu trúc cố định: sinh ra 7 đường kiểm thử nếu vòng lặp xác định được số lần lặp tối đa, hoặc 4 đường kiểm thử nếu không xác định. Ngược lại, kiểm thử động thực thi chương trình trong môi trường chạy và sử dụng kỹ thuật phủ định hệ ràng buộc, do đó nếu vòng lặp không có giới hạn lặp biết trước (như while (m!=n)), số ca kiểm thử sinh ra có thể rất lớn hoặc không xác định.

  3. Luận án phân loại các hướng tiếp cận chính trong giải ràng buộc xâu (String Constraint Solving) như thế nào?
    Luận án tổng hợp 3 hướng tiếp cận chính: (1) Tiếp cận dựa trên lý thuyết Otomat hữu hạn để biểu diễn và lưu trữ các phép toán trên xâu; (2) Tiếp cận dựa trên từ sử dụng các bộ giải lý thuyết thỏa mãn SMT; và (3) Tiếp cận dựa trên phân tách xâu thành các phần tử liền kề tương đương là số nguyên hoặc Bitvector.

  4. Kiến trúc mức cao của công cụ Java PathFinder (JPF) gồm những thành phần nào và chức năng của chúng ra sao?
    JPF được cấu thành từ hai thành phần chính: Java Virtual Machine (JVM) và Search. JVM có nhiệm vụ thực thi các chỉ thị Java bytecode để sinh ra các trạng thái cụ thể. Search đóng vai trò điều khiển (driver) lựa chọn trạng thái mà JVM cần xử lý, điều hướng JVM sinh trạng thái tiếp theo hoặc yêu cầu quay lui về trạng thái trước đó, đồng thời cấu hình và đánh giá các thuộc tính kiểm chứng.

  5. Quy trình thực thi biểu trưng động (DSE) xử lý đối tượng tham chiếu đầu vào bằng kỹ thuật gì?
    Khi xử lý phương thức nhận tham số là đối tượng tham chiếu (như SimpleList), DSE áp dụng kỹ thuật khởi tạo lười (lazy initialization). Các giá trị biểu trưng được gắn kết với trường của đối tượng thông qua cấu trúc ánh xạ $R(o)$, và việc khởi tạo cụ thể các liên kết đối tượng chỉ được thực hiện khi có các thao tác truy cập trường hoặc so sánh tham chiếu phát sinh trong quá trình thực thi.

Kết luận

Luận án đã nghiên cứu tổng quan về kiểm thử phần mềm, kỹ thuật thực thi biểu trưng và bài toán tự động sinh ca kiểm thử dựa trên mã nguồn chương trình. Nghiên cứu tập trung giải quyết các thách thức kỹ thuật trong mô hình hóa và giải quyết ràng buộc trên kiểu dữ liệu xâu và dữ liệu hỗn hợp thông qua sự kết hợp giữa lý thuyết Otomat và Bitvector. Các cải tiến được triển khai thử nghiệm trên nền tảng Java PathFinder (JPF), cung cấp cơ sở phương pháp và đóng góp kỹ thuật vào lĩnh vực kiểm chứng và tự động hóa kiểm thử phần mềm Java.