Tổng quan luận án

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 đồ UML" do nghiên cứu sinh Vũ Thị Đào 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 khoa học của PGS. Nguyễn Việt Hà, bảo vệ năm 2018 thuộc chuyên ngành Công nghệ thông tin (chuyên hướng Công nghệ phần mềm).

Trong quy trình phát triển phần mềm, hoạt động kiểm thử chiếm hơn 50% tổng nỗ lực phát triển [6], trong khi các lỗi phần mềm phát hiện được phụ thuộc chủ yếu vào chất lượng thiết kế kịch bản và dữ liệu kiểm thử. Phần lớn các giải pháp thực tế tập trung vào tự động hóa giai đoạn thực thi mã kiểm thử mà chưa chú trọng giai đoạn thiết kế. Việc sinh dữ liệu kiểm thử từ mã nguồn có nhược điểm là chỉ thực hiện được ở giai đoạn muộn, phụ thuộc vào công nghệ phân tích cú pháp của từng ngôn ngữ lập trình và dễ dẫn tới bùng nổ số lượng kịch bản. Ngược lại, kiểm thử dựa trên các đặc tả hình thức thuần túy (như Z, B) gặp rào cản lớn về tính khả thi và đòi hỏi chuyên gia chuyên sâu. Luận án lựa chọn hướng tiếp cận kiểm thử dựa trên mô hình (Model-Based Testing - MBT), cụ thể là các biểu đồ UML (Unified Modeling Language) kết hợp ngôn ngữ ràng buộc đối tượng OCL (Object Constraint Language), nhằm phát sinh kịch bản và dữ liệu kiểm thử tự động ngay từ giai đoạn thiết kế kiến trúc hệ thống.

Khoảng trống nghiên cứu được tác giả xác định gồm:

  • Các nghiên cứu hiện tại từ biểu đồ tuần tự UML mới chỉ giải quyết một số lượng hạn chế các toán tử (thường chỉ 5 toán tử cơ bản), chưa hỗ trợ đầy đủ toàn bộ 12 toán tử tương tác của chuẩn UML 2.0 cũng như các cấu trúc lồng ghép phức tạp.
  • Dữ liệu kiểm thử sinh ra chủ yếu giới hạn ở kiểu dữ liệu số cơ bản; thiếu giải pháp đối với các biến có cấu trúc dữ liệu động (con trỏ, cấu trúc liên kết) và các biểu thức ràng buộc chuỗi ký tự phức tạp.
  • Hiện tượng bùng nổ tổ hợp kịch bản kiểm thử, nguy cơ khóa chết (deadlock) và lỗi đồng bộ trong các luồng thực thi song song chưa được kiểm soát chặt chẽ bằng các tiêu chuẩn bao phủ tương tranh và bao phủ vòng lặp rõ ràng.

Mục tiêu nghiên cứu tổng quát của luận án là nghiên cứu, cải tiến, đề xuất và triển khai các phương pháp sinh tự động dữ liệu kiểm thử từ biểu đồ tuần tự UML 2.0 và biểu đồ lớp có ràng buộc OCL trong giai đoạn thiết kế kiểm thử, hướng tới mục tiêu tối thiểu hóa số lượng ca kiểm thử nhưng đạt độ bao phủ tối đa và nâng cao khả năng phát hiện lỗi.

Nhiệm vụ nghiên cứu cụ thể được phân định theo 4 nội dung:

  1. Tổng hợp, hệ thống hóa cơ sở lý thuyết và các nghiên cứu liên quan về kiểm thử dựa trên mô hình và kỹ thuật sinh dữ liệu kiểm thử tự động.
  2. Xây dựng phương pháp chuyển đổi biểu đồ tuần tự UML 2.0 sang mô hình đồ thị trung gian để giải quyết trọn vẹn 12 toán tử tương tác và cấu trúc lồng nhau; giải quyết hệ ràng buộc OCL cho kiểu dữ liệu số và biến có cấu trúc động.
  3. Thiết lập các tiêu chuẩn bao phủ tương tranh (yếu, trung bình, mạnh) và tiêu chuẩn bao phủ vòng lặp (lặp đơn, liền kề, lồng nhau) nhằm kiểm soát số lượng kịch bản kiểm thử, xử lý các lỗi tương tranh, khóa chết và đồng bộ dữ liệu.
  4. Đề xuất quy trình và thuật toán xử lý các ràng buộc chuỗi ký tự thông qua việc tích hợp, mở rộng bộ giải ràng buộc chuyên dụng.

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

  • Đối tượng nghiên cứu: Mô hình hành vi biểu diễn bằng biểu đồ tuần tự UML 2.0 và mô hình cấu trúc tĩnh biểu diễn bằng biểu đồ lớp kèm ràng buộc OCL.
  • Phạm vi nghiên cứu: Giai đoạn thiết kế kiểm thử (Test Design) trong quy trình kiểm thử phần mềm, tập trung vào hai tác vụ cốt lõi là sinh kịch bản kiểm thử (Test Scenario Generation) và giải ràng buộc sinh dữ liệu kiểm thử (Test Data Generation); kiểm nghiệm thực nghiệm thông qua các công cụ phần mềm tự xây dựng và các ca nghiên cứu điển hình (chức năng máy bán hàng tự động, chức năng chuyển tiền ngân hàng, chức năng xác thực thông tin ứng dụng web).

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

Luận án tổng kết bức tranh tổng thể các hướng tiếp cận sinh dữ liệu kiểm thử tự động theo cấu trúc phát triển qua thời gian và phân loại kỹ thuật:

Kiểm thử cấu trúc (Hộp trắng):

Kiểm thử chức năng (Hộp đen):

Kiểm thử dựa trên mô hình (Hộp xám):

Về các công cụ hiện hữu, tác giả khảo sát và phân loại dựa trên 4 tiêu chí: tính sẵn có (availability), độ trưởng thành (maturity), hoạt động duy trì (activity) và số trích dẫn (citation):

  • Spec Explorer [102]: Công cụ của Microsoft dựa trên mô hình đặc tả Spec#, sử dụng lý thuyết ôtômát kết hợp kỹ thuật kiểm thử tổ hợp và bộ giải SMT [48] để phát sinh ca kiểm thử.
  • Agedis [52, 51]: Dự án do Ủy ban Châu Âu tài trợ, sử dụng biểu đồ lớp, biểu đồ trạng thái, biểu đồ đối tượng UML và chỉ dẫn kịch bản bằng XML để tự động sinh ca kiểm thử.
  • UniTesK [14] (với các biến thể JavaTesK, CTesK): Phát sinh kiểm thử dựa trên việc duyệt không gian trạng thái đặc tả bị chặn bởi các vị từ tiêu chuẩn bao phủ.
  • Conformiq Qtronic [55]: Công cụ thương mại hỗ trợ kiểm thử hệ thống nhúng và giao dịch điện tử từ biểu đồ trạng thái UML, có khả năng xử lý hành vi không đơn định.

Về vị trí của luận án, tác giả chỉ ra các giới hạn nghiên cứu cụ thể mà công trình định vị giải quyết:

  • So với nghiên cứu của Micskei và cộng sự [72], vốn chỉ xử lý 5 toán tử (alt, opt, break, par, loop) và chỉ áp dụng cho biến số, phương pháp của luận án mở rộng cho toàn bộ 12 toán tử tương tác của UML 2.0 và xử lý bổ sung biến cấu trúc động.
  • So với nghiên cứu của Trung Dinh-Trong và cộng sự [30], vốn ánh xạ UML sang đồ thị tham số biến (VAG) và dùng Alloy Analyzer để sinh dữ liệu nhưng bị giới hạn về kiểu dữ liệu và chưa giải quyết trọn vẹn logic ba giá trị (true, false, undefined) của OCL, luận án xây dựng đồ thị dòng điều khiển trực tiếp và giải quyết logic OCL đầy đủ thông qua bảng chân lý và hàm vị từ.
  • So với các nghiên cứu của Sun [93], Samuel [89] và Khandai [58] về kiểm thử tương tranh từ biểu đồ hoạt động và tuần tự nhưng chưa đưa ra các tiêu chuẩn bao phủ định lượng hoặc chưa cài đặt kiểm chứng thực nghiệm, luận án định nghĩa rõ ba mức bao phủ tương tranh và giải quyết hiện tượng bùng nổ tổ hợp vết thực thi.

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

Cơ sở lý thuyết và khung phân tích

Luận án dựa trên khung lý thuyết của Kiểm thử dựa trên mô hình (Model-Based Testing - MBT) theo quy trình chuẩn 5 bước của Utting và Legeard [100]:

  1. Mô hình hóa hệ thống kiểm thử (SUT).
  2. Sinh các trừu tượng kiểm thử (abstract tests) từ mô hình.
  3. Cụ thể hóa các trừu tượng kiểm thử thành mã kiểm thử thực thi (concrete test scripts).
  4. Thực thi mã kiểm thử trên SUT.
  5. Phân tích kết quả, so sánh giá trị đầu ra thực tế với kết quả mong đợi.

Ngôn ngữ mô hình hóa thống nhất UML 2.0 [76] được sử dụng để mô tả khía cạnh động thông qua biểu đồ tuần tự với 12 toán tử phân đoạn kết hợp:

  1. alt (alternative): Lựa chọn rẽ nhánh loại trừ lẫn nhau dựa trên biểu thức bảo vệ (guard).
  2. opt (option): Nhánh tùy chọn, chỉ thực thi khi điều kiện bảo vệ đúng.
  3. loop: Vòng lặp với các tham số cận dưới (minint), cận trên (maxint) và biểu thức điều kiện boolean.
  4. break: Phân đoạn ngắt, thực thi thay thế cho phần còn lại của toán tử bao gói khi điều kiện thỏa mãn.
  5. par (parallel): Thực thi song song các toán hạng, cho phép các sự kiện đan xen tùy ý miễn là bảo toàn thứ tự cục bộ trên từng đường sống.
  6. seq (weak sequence): Trình tự yếu, duy trì thứ tự sự kiện trên cùng một đường sống nhưng cho phép đan xen tự do giữa các đường sống khác nhau.
  7. strict: Trình tự nghiêm ngặt, bắt buộc toàn bộ sự kiện của toán hạng trước phải hoàn thành trước toán hạng sau.
  8. critical: Vùng then chốt (vùng găng), cấm mọi sự kiện bên ngoài đan xen vào các đường sống thuộc vùng này.
  9. ignore: Bỏ qua các thông điệp được chỉ định, xem chúng không ảnh hưởng đến ngữ nghĩa kiểm thử.
  10. consider: Chỉ xem xét các thông điệp được liệt kê, mặc nhiên bỏ qua các thông điệp còn lại.
  11. neg (negative): Định nghĩa các vết tương tác không hợp lệ của hệ thống.
  12. assert: Khẳng định các vết tương tác bắt buộc phải xảy ra đúng như đặc tả.

Ngôn ngữ OCL 2.0 [77] được áp dụng trên biểu đồ lớp để biểu diễn các bất biến của lớp (inv), tiền điều kiện (pre) và hậu điều kiện (post) của phương thức.

Mô hình trung gian Đồ thị dòng điều khiển (Control Flow Graph - CFG) được định nghĩa hình thức là một bộ tứ: $$G = (A, E, in, F)$$ Trong đó:

  • $A$ là tập các đỉnh gồm 5 loại:
    • $BN$ (Basic Node): Nút khối lệnh biểu diễn thông điệp hoặc chuỗi thông điệp tuần tự.
    • $DN$ (Decision Node): Nút quyết định rẽ nhánh chứa biểu thức vị từ.
    • $MN$ (Merge Node): Nút hợp nhất các luồng điều khiển của toán tử lựa chọn (alt, opt).
    • $FN$ (Fork Node): Nút rẽ nhánh song song cho toán tử par và seq.
    • $JN$ (Join Node): Nút đồng bộ kết thúc của toán tử par và seq.
  • $in$ là nút khởi tạo; $F$ là tập các nút kết thúc.
  • $E = {(x, y) \mid x, y \in A \cup F}$ là tập các cạnh có hướng.
  • Cấu trúc chi tiết của mỗi nút $A_i \in A$ được chuẩn hóa dạng: $\langle noId, noType, noDetails, outEdge \rangle$. Trong đó $noDetails = \langle m_1, m_2, \dots, m_q \rangle$ chứa danh sách thông điệp, mỗi thông điệp gồm: $(m_i, parameterList, returnValue)$; mỗi tham số trong $parameterList$ lưu cấu trúc: $\langle name, dataType, value, constraint \rangle$. Mỗi cạnh ra thuộc $outEdge$ gồm: $\langle noId, predicate \rangle$.

Tiêu chuẩn bao phủ và kỹ thuật đo lường

Luận án thiết lập hai nhóm tiêu chuẩn bao phủ chuyên biệt:

  1. Tiêu chuẩn bao phủ tương tranh [95, 93]:

    • Bao phủ tương tranh yếu: Mỗi tiến trình song song chỉ cần thực thi qua một tuần tự khả thi, không xét sự đan xen giữa các thông điệp.
    • Bao phủ tương tranh trung bình: Bao phủ tất cả các tuần tự khả thi của các tiến trình song song nhưng không xét sự đan xen thông điệp.
    • Bao phủ tương tranh mạnh: Bao phủ tất cả các tuần tự khả thi có xét sự đan xen đầy đủ giữa các thông điệp của các tiến trình song song.

  2. Tiêu chuẩn bao phủ vòng lặp: Phân loại theo cấu trúc gồm: lặp đơn giản, lặp liền kề và lặp lồng nhau. Để kiểm tra giá trị biên và trạng thái lặp, tác giả xác định 7 trường hợp số lần lặp mục tiêu:

    • Vòng lặp thực hiện 0 lần.
    • Vòng lặp thực hiện 1 lần.
    • Vòng lặp thực hiện 2 lần.
    • Vòng lặp thực hiện $k$ lần ($2 < k < n - 1$, với $n$ là số lần lặp tối đa).
    • Vòng lặp thực hiện $n - 1$ lần.
    • Vòng lặp thực hiện $n$ lần.
    • Vòng lặp thực hiện $n + 1$ lần (áp dụng khi mô hình cho phép kiểm tra lỗi vượt biên).

  3. Độ phân tích đột biến (Mutation Score - MS) [94, 28]: Được áp dụng để đo lường định lượng năng lực phát hiện lỗi của tập dữ liệu kiểm thử theo công thức: $$MS = \frac{N_k}{N_m - N_e}$$ Trong đó: $N_k$ là số lượng đột biến bị tiêu diệt (killed mutants); $N_m$ là tổng số đột biến được cấy vào chương trình; $N_e$ là số lượng đột biến tương đương (equivalent mutants).

Nguồn dữ liệu thực nghiệm

Dữ liệu mô hình hóa đầu vào được trích xuất từ tài liệu XMI (XML Metadata Interchange) chuẩn hóa của các ca nghiên cứu:

  • Hệ thống máy bán hàng tự động (Vending Machine).
  • Hệ thống thực hiện chức năng chuyển tiền ngân hàng (Bank Transfer).
  • Chức năng kiểm tra và xác thực thông tin người dùng trong ứng dụng web.

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

Chương 1: Giới thiệu

Chương 1 thiết lập bài toán kiểm thử dựa trên mô hình trong công nghệ phần mềm, phân tích sự cần thiết của việc dịch chuyển hoạt động kiểm thử về các pha sớm của vòng đời phát triển. Tác giả phân tích các hạn chế của việc sinh kiểm thử từ mã nguồn và từ đặc tả hình thức, từ đó xác lập tính cấp thiết của việc sinh dữ liệu kiểm thử từ biểu đồ UML. Chương này xác định rõ phương pháp tiếp cận từ trên xuống (top-down), tổng hợp phạm vi nghiên cứu tập trung vào biểu đồ tuần tự UML 2.0 và biểu đồ lớp có ràng buộc OCL, cấu trúc hóa 4 mục tiêu nghiên cứu và phác thảo cấu trúc 6 chương của luận án.

Chương 2: Kiến thức nền tảng

Chương 2 hệ thống hóa toàn diện cơ sở lý thuyết về kiểm thử phần mềm, quy trình kiểm thử dựa trên mô hình 5 bước và các khái niệm ca kiểm thử, dữ liệu kiểm thử, kịch bản kiểm thử, tiêu chuẩn bao phủ. Tác giả phân tích chi tiết cú pháp và ngữ nghĩa của 12 toán tử tương tác trong chuẩn UML 2.0, biểu thức ràng buộc OCL (bất biến, tiền/hậu điều kiện), cấu trúc hình thức của đồ thị dòng điều khiển CFG với 5 loại nút cơ bản. Đồng thời, chương này tổng quan các độ bao phủ tương tranh, độ bao phủ vòng lặp, lý thuyết kiểm thử đột biến và công thức tính MS. Phần cuối chương điểm luận các phương pháp sinh dữ liệu kiểm thử tĩnh, động, kết hợp, kiểm thử ngẫu nhiên, thực thi tượng trưng, DART và đánh giá ưu nhược điểm của 4 công cụ điển hình: Spec Explorer, Agedis, UniTesK, Conformiq Qtronic.

Chương 3: Sinh dữ liệu kiểm thử cho kiểu dữ liệu số và cấu trúc động

Chương 3 trình bày giải pháp giải quyết trọn vẹn 12 toán tử tương tác của UML 2.0 và các cấu trúc lồng nhau. Quy trình đề xuất gồm các bước:

  1. Chuẩn hóa tệp XMI biểu diễn biểu đồ tuần tự và biểu đồ lớp.
  2. Ánh xạ các toán tử UML sang các mẫu đồ thị con trong CFG.
  3. Sinh kịch bản kiểm thử bằng thuật toán duyệt đồ thị (DFS/BFS).
  4. Chuyển đổi các biểu thức điều kiện OCL gắn trên cạnh CFG thành các hàm vị từ (predicate functions) dựa trên bảng chân lý logic OCL và toán tử quan hệ số học.
  5. Giải hệ hàm vị từ để sinh dữ liệu kiểm thử cho biến số và cấu trúc động (biến con trỏ, cấu trúc liên kết).

Tác giả thiết kế và cài đặt công cụ thực nghiệm mang tên SequenceTesting. Kết quả thực nghiệm trên chức năng máy bán hàng tự động và các cấu trúc dữ liệu động được so sánh với phương pháp của Micskei [72] và Trung Dinh-Trong [30], chứng minh phương pháp bao phủ được các cấu trúc lồng nhau phức tạp và các biến dạng con trỏ mà các công cụ trước đó bỏ qua.

Chương 4: Sinh dữ liệu kiểm thử cho vòng lặp và các ứng dụng tương tranh

Chương 4 tập trung giải quyết bài toán bùng nổ không gian trạng thái, hiện tượng khóa chết (deadlock) và lỗi đồng bộ dữ liệu trong các phân đoạn thực thi song song (par, seq) và phân đoạn lặp (loop). Tác giả đề xuất thuật toán phát sinh kịch bản kiểm thử dựa trên ba mức bao phủ tương tranh (yếu, trung bình, mạnh) và thuật toán sinh dữ liệu kiểm thử vòng lặp phát triển từ kỹ thuật giảm miền động (DDR) của Gupta [75], tính toán điểm chia miền giá trị (split points) để bao phủ đầy đủ các biên lặp (0, 1, 2, $k$, $n-1$, $n$, $n+1$).

Tác giả xây dựng công cụ thực nghiệm SequenceConcur, áp dụng kiểm thử trên chức năng chuyển tiền ngân hàng. Kết quả thực nghiệm đo lường bằng độ phân tích đột biến (MS) được đối sánh trực tiếp với phương pháp kiểm thử ngẫu nhiên và phương pháp của Samuel [95], cho thấy bộ kịch bản kiểm thử sinh ra có khả năng tiêu diệt đột biến vượt trội trong các tình huống tranh chấp tài nguyên và lỗi biên vòng lặp.

Chương 5: Sinh dữ liệu kiểm thử cho kiểu dữ liệu chuỗi

Chương 5 giải quyết bài toán sinh dữ liệu kiểm thử đối với các ràng buộc chuỗi ký tự phức tạp trong biểu đồ UML (thường xuất hiện trong các ứng dụng web và hệ thống thông tin). Tác giả phân tích ngữ nghĩa các toán tử chuỗi, cấu trúc ngữ pháp ràng buộc và các quy tắc giảm (reduction rules) của bộ giải Z3-str [114]. Trên cơ sở đó, luận án đề xuất mở rộng bộ giải Z3-str bằng cách bổ sung các quy tắc tiền xử lý và quy tắc rút gọn đệ quy cho hai hàm xử lý chuỗi phổ biến nhưng phức tạp là search và replaceAll.

Quy trình được tích hợp trong công cụ thực nghiệm SeqString. Thực nghiệm so sánh khả năng tìm lỗi và hiệu năng xử lý toán tử chuỗi giữa SeqString với phương pháp của nhóm tác giả Shoichiro [39] trên chức năng kiểm tra thông tin ứng dụng web, khẳng định tốc độ giải ràng buộc chuỗi và tỷ lệ phát hiện lỗi cấu trúc chuỗi đạt độ chính xác cao.

Chương 6: Kết luận

Chương 6 tổng kết các kết quả đạt được của luận án, khẳng định việc hoàn thành các mục tiêu nghiên cứu đề ra trong giai đoạn thiết kế kiểm thử từ biểu đồ UML. Đồng thời, tác giả chỉ ra các giới hạn hiện tại và vạch ra các hướng nghiên cứu tiếp theo nhằm hoàn thiện giải pháp.

Bảng tổng hợp đối sánh kỹ thuật của luận án

Dưới đây là bảng tổng hợp đối sánh giữa phương pháp đề xuất trong luận án với các nghiên cứu và công cụ liên quan được tác giả phân tích trong văn bản:

Tiêu chí so sánh Nghiên cứu Micskei [72] Nghiên cứu Dinh-Trong [30] Nghiên cứu Sun [93] / Samuel [95] Đề xuất của Luận án (SequenceTesting, SequenceConcur, SeqString)
Mô hình đầu vào Biểu đồ tuần tự UML Biểu đồ UML + OCL Biểu đồ hoạt động / tuần tự UML Biểu đồ tuần tự UML 2.0 + Biểu đồ lớp (OCL)
Toán tử UML hỗ trợ 5 toán tử (alt, opt, break, par, loop) Hạn chế, không đầy đủ Tập trung vào luồng rẽ nhánh và song song Toàn bộ 12 toán tử chuẩn UML 2.0, hỗ trợ lồng ghép
Kiểu dữ liệu giải quyết Kiểu dữ liệu số Kiểu dữ liệu số, hạn chế kiểu cấu trúc Dữ liệu ngẫu nhiên, số cơ bản Kiểu số, cấu trúc động (con trỏ), chuỗi ký tự (search, replaceAll)
Mô hình trung gian CFG đơn giản Đồ thị tham số biến (VAG) / Alloy Cây nhị phân / Đồ thị luồng Đồ thị dòng điều khiển CFG chuẩn hóa ($BN, DN, MN, FN, JN$)
Xử lý tương tranh Không xét tiêu chuẩn bao phủ Không chuyên sâu Không phân chia mức bao phủ rõ ràng Ba mức bao phủ tương tranh: Yếu, Trung bình, Mạnh
Kiểm thử vòng lặp Tối đa 1 lần lặp Không tối ưu hóa biên Chưa xử lý đa mức lặp 7 trường hợp lặp biên và đại diện (0, 1, 2, $k$, $n-1$, $n$, $n+1$)
Bộ giải ràng buộc Hàm cực tiểu hóa số học Alloy Analyzer Sinh ngẫu nhiên Hàm vị từ OCL, kỹ thuật giảm miền DDR cải tiến, Z3-str mở rộng
Công cụ cài đặt Thử nghiệm cục bộ Chuyển đổi Alloy Prototype thực nghiệm Bộ công cụ chuyên biệt: SequenceTesting, SequenceConcur, SeqString

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

Luận án tự xác định các đóng góp mới về mặt lý luận khoa học và thực tiễn kỹ thuật phần mềm bao gồm:

  1. Đóng góp về quy trình chuyển đổi và bao phủ toán tử UML 2.0:

    • Đề xuất quy trình hình thức hóa và chuyển đổi hoàn chỉnh biểu đồ tuần tự UML 2.0 sang đồ thị dòng điều khiển trung gian CFG, xử lý trọn vẹn tất cả 12 toán tử tương tác (kể cả các toán tử phức tạp như strict, critical, ignore, consider, assert, neg) và các cấu trúc khối lệnh lồng nhau phức tạp.
    • Xây dựng cơ chế trích xuất và ánh xạ các ràng buộc OCL từ biểu đồ lớp thành hệ các hàm vị từ xử lý đầy đủ miền giá trị logic ba trạng thái (true, false, undefined).
    • Mở rộng thuật toán sinh dữ liệu kiểm thử tự động từ kiểu dữ liệu số sang kiểu dữ liệu có cấu trúc động (biến con trỏ và danh sách cấu trúc).

  2. Đóng góp về kiểm thử ứng dụng tương tranh và cấu trúc lặp:

    • Định nghĩa và áp dụng hệ thống ba tiêu chuẩn bao phủ tương tranh (yếu, trung bình, mạnh) trên biểu đồ tuần tự, cho phép kiểm soát số lượng kịch bản kiểm thử sinh ra nhằm ngăn chặn hiện tượng bùng nổ tổ hợp vết thực thi.
    • Đề xuất giải pháp phát hiện sớm các nguy cơ khóa chết (deadlock) và lỗi đồng bộ trong các luồng thực thi song song có chia sẻ dữ liệu hoặc không chia sẻ dữ liệu.
    • Thiết lập thuật toán kiểm thử vòng lặp chuyên sâu dựa trên kỹ thuật giảm miền động (DDR), tự động tính toán điểm chia miền để tạo ra các bộ dữ liệu kiểm thử thỏa mãn 7 trường hợp số lần lặp đặc trưng.

  3. Đóng góp về giải quyết hệ ràng buộc kiểu chuỗi ký tự:

    • Mở rộng lý thuyết ngữ pháp và quy tắc giảm của bộ giải Z3-str, bổ sung các quy tắc tiền xử lý và quy tắc rút gọn đệ quy chuyên biệt cho hai toán tử chuỗi phức tạp là search và replaceAll.
    • Nâng cao hiệu năng giải các hệ ràng buộc chuỗi trong kiểm thử các ứng dụng hướng dịch vụ và ứng dụng web mô hình hóa bằng UML.

  4. Đóng góp về mặt công cụ và thực nghiệm:

    • Thiết kế kiến trúc và cài đặt hoàn chỉnh ba công cụ phần mềm thực nghiệm: SequenceTesting, SequenceConcur, và SeqString.
    • Thực hiện kiểm nghiệm thực nghiệm trên các ca nghiên cứu thực tế, sử dụng độ đo bao phủ đường dẫn và độ phân tích đột biến (Mutation Score - MS) để chứng minh năng lực phát hiện lỗi phần mềm của các tập dữ liệu kiểm thử được sinh ra.

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

Dựa trên phạm vi và các nội dung được văn bản đề cập, luận án ghi nhận các giới hạn kỹ thuật và phương hướng phát triển tiếp theo:

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

  • Giới hạn pha kiểm thử: Nghiên cứu chỉ tập trung giải quyết giai đoạn thiết kế kiểm thử (sinh kịch bản và dữ liệu kiểm thử trừu tượng), việc chuyển đổi sang mã kiểm thử cụ thể và thực thi kiểm thử tự động vẫn phụ thuộc vào ngôn ngữ lập trình đích và môi trường thực thi cụ thể của SUT.
  • Phụ thuộc vào chất lượng mô hình: Phương pháp giả định mô hình biểu đồ tuần tự UML và biểu đồ lớp có ràng buộc OCL đầu vào đã được chuẩn hóa và chính xác. Nếu mô hình thiết kế ban đầu chứa sai sót logic hoặc thiếu nhất quán, dữ liệu kiểm thử sinh ra sẽ không phản ánh đúng hành vi mong muốn của hệ thống.
  • Thách thức về bài toán Test Oracle: Luận án giải quyết bài toán sinh dữ liệu đầu vào ($Test\ Data$) thỏa mãn các đường dẫn, nhưng việc tự động sinh hoàn toàn giá trị đầu ra mong đợi ($Expected\ Output$) cho mọi ca kiểm thử phức tạp từ biểu đồ tuần tự vẫn là thách thức lớn của phương pháp kiểm thử dựa trên mô hình nói chung.
  • Phạm vi biểu đồ: Mới tập trung khai thác biểu đồ tuần tự kết hợp biểu đồ lớp, chưa tích hợp tự động đồng thời với các biểu đồ hành vi khác như biểu đồ trạng thái (State Machine) hay biểu đồ hoạt động (Activity Diagram) trong cùng một chu trình sinh kiểm thử thống nhất.

Hướng nghiên cứu tiếp theo (trình bày tại Mục 6.2)

  • Tiếp tục mở rộng và hoàn thiện các thuật toán nhằm sinh dữ liệu kiểm thử tự động cho các hệ thống phần mềm có quy mô lớn hơn và kiến trúc phân tán phức tạp hơn.
  • Nghiên cứu cơ chế tự động hóa hoàn toàn quá trình tạo giá trị đầu ra mong đợi (Test Oracle) cho các kịch bản kiểm thử dựa trên việc phân tích sâu ngữ nghĩa của các hậu điều kiện OCL.
  • Tích hợp kết hợp nhiều loại biểu đồ UML khác nhau (biểu đồ trạng thái, biểu đồ hoạt động và biểu đồ tuần tự) để tối ưu hóa độ bao phủ kiểm thử ở cả mức kiểm thử đơn vị, kiểm thử tích hợp và kiểm thử hệ thống.
  • Phát triển và đóng gói các công cụ thực nghiệm thành các module mở rộng tích hợp trực tiếp vào các môi trường phát triển phần mềm (IDE) hoặc các công cụ thiết kế mô hình chuẩn CASE hiện nay.

Giá trị tham khảo

Luận án là tài liệu kỹ thuật chuyên khảo phục vụ trực tiếp cho các nhóm đối tượng học thuật và ứng dụng thực tiễn:

  • Nghiên cứu sinh và học viên cao học ngành Khoa học máy tính, Kỹ thuật phần mềm:
    • Cung cấp phương pháp luận hình thức hóa mô hình thiết kế UML thành cấu trúc dữ liệu đồ thị CFG phục vụ tính toán tự động.
    • Cung cấp khung tài liệu tham khảo chi tiết về lý thuyết kiểm thử đột biến, kỹ thuật giảm miền động (DDR) và cơ chế giải các ràng buộc chuỗi bằng bộ giải SMT/Z3-str mở rộng.
  • Giảng viên và chuyên gia giảng dạy môn Kiểm thử phần mềm, Đảm bảo chất lượng phần mềm (QA), Kỹ nghệ phần mềm:
    • Sử dụng Chương 2 như giáo trình tham khảo chuyên sâu về Kiểm thử dựa trên mô hình (MBT), các chuẩn bao phủ tương tranh, bao phủ vòng lặp và phân loại các công cụ MBT quốc tế (Spec Explorer, Agedis, UniTesK, Conformiq Qtronic).
    • Sử dụng các ví dụ hình thức hóa trong Chương 3, 4, 5 (như máy bán hàng, chức năng ngân hàng, ứng dụng web) làm học liệu bài tập lớn và dự án môn học.
  • Kỹ sư kiểm thử, kiến trúc sư phần mềm và nhóm phát triển công cụ (Testing Tool Developers):
    • Tham khảo kiến trúc thiết kế của ba công cụ thực nghiệm: SequenceTesting (xử lý 12 toán tử UML 2.0 và con trỏ), SequenceConcur (kiểm thử song song, vòng lặp, kiểm soát deadlock), và SeqString (giải ràng buộc chuỗi ký tự).
    • Áp dụng các quy tắc ánh xạ cú pháp XMI sang CFG để xây dựng các plugin sinh kiểm thử tự động từ mô hình trong các dự án công nghiệp.

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

1. Luận án giải quyết những toán tử tương tác nào của biểu đồ tuần tự UML 2.0?

Luận án hỗ trợ trọn vẹn toàn bộ 12 toán tử tương tác của chuẩn UML 2.0, bao gồm:

  • Nhóm lựa chọn và rẽ nhánh: alt (alternative), opt (option).
  • Nhóm lặp và điều khiển luồng: loop (vòng lặp với cận minint, maxint), break (ngắt phân đoạn).
  • Nhóm tương tranh và tuần tự: par (thực thi song song), seq (trình tự yếu), strict (trình tự nghiêm ngặt), critical (vùng găng / vùng then chốt).
  • Nhóm bộ lọc thông điệp: ignore (bỏ qua thông điệp xác định), consider (chỉ xét các thông điệp xác định).
  • Nhóm kiểm chứng hợp lệ: neg (vết tương tác không hợp lệ), assert (vết tương tác khẳng định hợp lệ). Phương pháp xử lý được cả các trường hợp các toán tử này lồng ghép phức tạp vào nhau.

2. Mô hình đồ thị dòng điều khiển (CFG) trung gian được định nghĩa như thế nào?

CFG được định nghĩa là một bộ tứ $G = (A, E, in, F)$, trong đó $A$ là tập các nút, $E$ là tập các cạnh có hướng, $in$ là nút khởi tạo và $F$ là tập các nút kết thúc. Tập nút $A$ gồm 5 loại:

  • $BN$ (Basic Node): Biểu diễn các thông điệp tuần tự.
  • $DN$ (Decision Node): Biểu diễn các biểu thức vị từ rẽ nhánh.
  • $MN$ (Merge Node): Nút hợp nhất luồng rẽ nhánh của alt, opt.
  • $FN$ (Fork Node): Đầu vào tách luồng song song của par, seq.
  • $JN$ (Join Node): Đầu ra hợp luồng song song của par, seq. Mỗi nút $A_i$ chứa bộ thông tin: $\langle noId, noType, noDetails, outEdge \rangle$, lưu trữ đầy đủ định danh, loại nút, danh sách thông điệp kèm tham số/ràng buộc OCL và danh sách cạnh ra kèm điều kiện vị từ.

3. Ba tiêu chuẩn bao phủ tương tranh được áp dụng trong luận án gồm những gì?

Luận án áp dụng ba tiêu chuẩn bao phủ tương tranh:

  1. Bao phủ tương tranh yếu: Sinh các ca kiểm thử bao phủ chỉ một tuần tự khả thi của các tiến trình song song, không cho phép có sự đan xen giữa các thông điệp của các tiến trình đó.
  2. Bao phủ tương tranh trung bình: Sinh các ca kiểm thử bao phủ tất cả các tuần tự khả thi của các tiến trình song song, không cho phép có sự đan xen giữa các thông điệp của các tiến trình đó.
  3. Bao phủ tương tranh mạnh: Sinh các ca kiểm thử bao phủ tất cả các tuần tự khả thi của các tiến trình song song có xét sự đan xen giữa các thông điệp của các tiến trình song song.

4. Thuật toán kiểm thử vòng lặp của luận án kiểm tra những trường hợp số lần lặp nào?

Đối với một vòng lặp có số lần lặp tối đa là $n$, luận án xác định 7 trường hợp số lần lặp cần sinh dữ liệu kiểm thử:

  • Lặp 0 lần (không thực hiện thân vòng lặp).
  • Lặp 1 lần.
  • Lặp 2 lần.
  • Lặp $k$ lần (với $2 < k < n - 1$, đại diện cho giá trị điển hình ở giữa miền lặp).
  • Lặp $n - 1$ lần (cận biên dưới của số lần lặp tối đa).
  • Lặp $n$ lần (số lần lặp tối đa cho phép).
  • Lặp $n + 1$ lần (trường hợp vượt biên để phát hiện lỗi kiểm tra điều kiện lặp, nếu mô hình cho phép). Nếu không xác định được $n$, phương pháp sinh kiểm thử cho 4 trường hợp đầu tiên. Đối với vòng lặp liền kề, kiểm thử tuần tự từ trên xuống; đối với vòng lặp lồng nhau, kiểm thử tuần tự từ trong ra ngoài.

5. Năng lực tìm lỗi của các bộ dữ liệu kiểm thử được đánh giá định lượng bằng công cụ và chỉ số nào?

Năng lực tìm lỗi được đánh giá định lượng bằng kỹ thuật kiểm thử đột biến thông qua Độ đo đột biến (Mutation Score - MS) theo công thức: $$MS = \frac{N_k}{N_m - N_e}$$ Trong đó $N_k$ là số đột biến bị bộ dữ liệu kiểm thử tiêu diệt, $N_m$ là tổng số đột biến cấy vào mã nguồn, $N_e$ là số đột biến tương đương. Giá trị MS càng cao chứng minh tập kịch bản và dữ liệu kiểm thử sinh ra có khả năng phát hiện lỗi càng lớn. Hiệu năng này được kiểm chứng qua ba công cụ do tác giả cài đặt là SequenceTesting, SequenceConcur và SeqString.

Kết luận

Luận án tiến sĩ của tác giả Vũ Thị Đào đã giải quyết bài toán sinh tự động kịch bản và dữ liệu kiểm thử từ các mô hình thiết kế UML 2.0 và ràng buộc OCL trong giai đoạn thiết kế phần mềm. Công trình đã chuẩn hóa quy trình ánh xạ biểu đồ tuần tự sang đồ thị dòng điều khiển trung gian CFG để xử lý trọn vẹn 12 toán tử tương tác, giải quyết thành công các hệ ràng buộc cho kiểu dữ liệu số, cấu trúc động (biến con trỏ) và chuỗi ký tự thông qua mở rộng bộ giải Z3-str. Đồng thời, việc thiết lập các tiêu chuẩn bao phủ tương tranh ba mức và tiêu chuẩn bao phủ vòng lặp 7 trường hợp biên đã giúp kiểm soát hiện tượng bùng nổ tổ hợp kịch bản và nâng cao năng lực phát hiện các lỗi tương tranh, khóa chết và đồng bộ dữ liệu. Kết quả nghiên cứu được đóng gói thành ba công cụ phần mềm thực nghiệm SequenceTesting, SequenceConcur, SeqString và được kiểm chứng định lượng bằng độ phân tích đột biến, đóng góp thiết thực cho hướng tiếp cận kiểm thử phần mềm dựa trên mô hình.