Tổng quan về luận án

Kiểm thử phần mềm (Software Testing) đóng vai trò quyết định trong việc bảo đảm chất lượng hệ thống nhưng lại tiêu tốn từ 30% đến 60% tổng chi phí và thời gian phát triển phần mềm toàn diện [71]. Trong bối cảnh các yêu cầu chức năng biến đổi liên tục trong suốt vòng đời dự án, việc tái kiểm thử và duy trì bộ kiểm thử (regression testing) thủ công tạo ra áp lực khổng lồ về nhân lực và ngân sách. Mặc dù kiểm thử tự động đã đạt được nhiều tiến bộ ở pha thực thi (test execution), khâu mô hình hóa yêu cầu và tự động hóa sinh ca kiểm thử (automated test case generation) vẫn là nút thắt cổ chai lớn chưa được giải quyết triệt để. Luận án tiến sĩ của Nghiên cứu sinh Chu Thị Minh Huệ với đề tài "Kiểm thử dựa trên mô hình với cách tiếp cận mô hình hóa chuyên biệt miền" (chuyên ngành Công nghệ Thông tin, Trường Đại học Công nghệ – Đại học Quốc gia Hà Nội) đã đề xuất một giải pháp đột phá, tích hợp kỹ thuật Kiểm thử dựa trên mô hình (Model-Based Testing – MBT) với Phương pháp Mô hình hóa chuyên biệt miền (Domain-Specific Modeling – DSM) nhằm tự động hóa hoàn toàn quy trình sinh ca kiểm thử chức năng mức hệ thống.

Khoảng trống nghiên cứu (Research Gap) cốt lõi xuất phát từ thực tế các đặc tả yêu cầu bằng ngôn ngữ tự nhiên theo mẫu (Restricted Natural Language – RNL) tuy dễ tiếp cận với các bên liên quan phi kỹ thuật nhưng lại thiếu ngữ nghĩa hình thức, đòi hỏi các kỹ thuật xử lý ngôn ngữ tự nhiên (NLP) phức tạp, phụ thuộc ngôn ngữ và khó trích xuất chính xác các ràng buộc logic [58, 73]. Mặt khác, các phương pháp sử dụng biểu đồ chuẩn UML (như Activity Diagram, Sequence Diagram) chỉ tập trung vào việc trích xuất kịch bản trừu tượng (abstract test scenarios) mà bỏ qua việc sinh dữ liệu kiểm thử cụ thể (concrete test data) và không nắm bắt được trạng thái bên trong của hệ thống [24, 51, 67]. Thêm vào đó, các ngôn ngữ chuyên biệt miền hiện hữu như NDT [16, 23], RSL/TSL [63, 65] hay SelabReq [59] hoặc chỉ mô tả dữ liệu dưới dạng điều kiện định tính, hoặc không hỗ trợ sinh kiểm thử, hoặc thiếu cơ chế tích hợp đồng thời vào quy trình Phát triển phần mềm hướng mô hình (Model-Driven Development – MDD).

Luận án tập trung giải quyết 4 câu hỏi nghiên cứu trọng tâm (Research Questions):

  1. RQ1: Làm thế nào để định nghĩa một ngôn ngữ mô hình hóa chuyên biệt miền (DSML) cho phép đặc tả ca sử dụng vừa trực quan, dễ hiểu với chuyên gia miền, vừa có ngữ nghĩa hình thức chặt chẽ để tích hợp vào MDD?
  2. RQ2: Cấu trúc thông tin và siêu mô hình (metamodel) nào cần thiết cho một ngôn ngữ đặc tả ca kiểm thử (TCSL) để làm đầu vào trực tiếp cho các công cụ tự động sinh và thực thi tập lệnh kiểm thử (test scripts)?
  3. RQ3: Phương pháp chuyển đổi mô hình (Model Transformation) nào có thể kết hợp mô hình hành vi ca sử dụng và mô hình lớp khái niệm miền nhằm sinh tự động các kịch bản kiểm thử đạt tiêu chí bao phủ tối ưu cùng dữ liệu kiểm thử cụ thể thỏa mãn các ràng buộc nghiệp vụ?
  4. RQ4: Bộ công cụ tích hợp trên nền tảng kỹ nghệ hướng mô hình (MDE) cần được thiết kế và thực thi như thế nào để chứng minh tính khả thi, độ chính xác và khả năng ứng dụng thực tế của phương pháp?

Khung lý thuyết của luận án thiết lập trên nền tảng lý thuyết Kiểm thử dựa trên mô hình (MBT) [9, 56], Kỹ nghệ hướng mô hình (MDE/MDD) dựa trên chuẩn Eclipse Modeling Framework (EMF) [21], Hệ thống chuyển trạng thái được gán nhãn (Labelled Transition System – LTS) để định nghĩa ngữ nghĩa hình thức, cùng Ngôn ngữ ràng buộc đối tượng (Object Constraint Language – OCL) của nhóm OMG [30].

Quy mô thực nghiệm của nghiên cứu được tiến hành trên các ca sử dụng chuẩn hóa và phức tạp như hệ thống Ngân hàng tự động ATM (chức năng Rút tiền - Withdraw), hệ thống Quản trị thư viện số (Lend Book), và hệ thống Đăng ký khóa học trực tuyến. Đóng góp đột phá của luận án được định lượng thông qua việc tự động hóa 100% đường dẫn kiểm thử, đảm bảo tiêu chí phủ đường hoạt động (Activity Path Coverage) [39] bao gồm cả vòng lặp (với $k \in {0, 1, 2}$ lần lặp) và các hành vi đồng thời (concurrency), tự động giải quyết không gian ràng buộc OCL thông qua công cụ USE (UML-based Specification Environment) nhằm tạo ra các thể hiện đối tượng (Object Diagrams) chứa dữ liệu kiểm thử chính xác và trạng thái hệ thống tiền điều kiện.

Literature Review và Positioning

Quy trình MBT truyền thống bao gồm 5 pha cơ bản: (1) Mô hình hóa hệ thống (Modeling), (2) Sinh ca kiểm thử (Test case generation), (3) Sinh tập lệnh thực thi (Test script generation), (4) Thực thi kiểm thử (Test execution), và (5) Phân tích kết quả (Test analysis) [9]. Trong khi 3 pha sau đã được hoàn thiện bởi các công cụ thương mại và mã nguồn mở (như Selenium, JUnit, TestComplete), hai pha đầu tiên vẫn là thách thức nghiên cứu lớn nhất.

+-----------------------------------------------------------------------------------+
|                           QUY TRÌNH KIỂM THỬ DỰA TRÊN MÔ HÌNH (MBT)               |
+-----------------------------------------------------------------------------------+
|  [Pha 1: Mô hình hóa]    --->   [Pha 2: Sinh ca kiểm thử]   --->  [Pha 3, 4, 5:   |
|  - USL Metamodel                - USLTG Algorithm                  Thực thi &     |
|  - Domain Class Model           - USE OCL Solver                   Báo cáo]       |
|  - LTS Semantics                - TCSL Metamodel                   (Công cụ KDTF) |
+-----------------------------------------------------------------------------------+

Tổng quan y văn quốc tế ghi nhận hai nhánh tiếp cận chính trong việc sinh ca kiểm thử từ ca sử dụng:

  1. Nhánh tiếp cận dựa trên ngôn ngữ tự nhiên bán cấu trúc (Restricted Natural Language - RNL) và Xử lý ngôn ngữ tự nhiên (NLP): Yue et al. [73] và Wang et al. [58] phát triển phương pháp RUCM (Restricted Use Case Modeling), sử dụng 26 từ khóa và các quy tắc cú pháp nghiêm ngặt để hạn chế sự mơ hồ của ngôn ngữ tự nhiên, sau đó áp dụng NLP để sinh mô hình trung gian (UCTM) phục vụ sinh ca kiểm thử. Tuy nhiên, luồng nghiên cứu này gặp phải mâu thuẫn lớn: nếu nới lỏng cú pháp, công cụ NLP sẽ gặp lỗi phân tích ngữ nghĩa (semantic ambiguity); nếu thắt chặt cú pháp, người viết đặc tả sẽ gặp rào cản kỹ thuật rất lớn. Hơn nữa, RNL hoàn toàn không có cú pháp trừu tượng (abstract syntax) hình thức, khiến việc kiểm chứng tính đúng đắn và tự động trích xuất các ràng buộc logic toán học để sinh dữ liệu kiểm thử cụ thể trở nên bất khả thi.

  2. Nhánh tiếp cận dựa trên mô hình hóa UML chuẩn (Standard UML-based approaches): Các công trình của Briand et al. [7], Shen et al. [51] và Linzhang et al. [67] đề xuất chuyển đổi mô tả ca sử dụng sang Activity Diagram hoặc Sequence Diagram để trích xuất các đường đi thực thi (execution paths). Mặc dù giải quyết được tính trực quan và phân tách rõ hành động giữa Tác nhân (Actor) và Hệ thống (System), các kỹ thuật này chỉ sinh ra các ca kiểm thử trừu tượng (kịch bản kiểm thử) mà không xác định được giá trị cụ thể của biến đầu vào cũng như trạng thái cơ sở dữ liệu nội tại trước khi thực thi.

+---------------------+-------------------------------+----------------------------------+
| Phương pháp / DSML  | Đặc tả ca sử dụng & Ngữ nghĩa | Mức độ chi tiết của Ca kiểm thử  |
+---------------------+-------------------------------+----------------------------------+
| RUCM [58, 73]       | Ngôn ngữ tự nhiên bị giới hạn | Kịch bản trừu tượng, dữ liệu mô  |
|                     | (RNL), xử lý qua NLP, informal| tả chung chung, thiếu OCL solver |
+---------------------+-------------------------------+----------------------------------+
| NDT [16, 23]        | DSML hướng Web (Navigational),| Trích xuất kịch bản điều hướng,  |
|                     | cú pháp đồ họa                | không xác định giá trị đầu vào   |
+---------------------+-------------------------------+----------------------------------+
| RSL / TSL [63, 65]  | DSML mức yêu cầu (RSL), tích  | Đặc tả kiểm thử TSL chỉ chứa     |
|                     | hợp công cụ ReDSeeDS          | điều kiện định tính, không có số |
+---------------------+-------------------------------+----------------------------------+
| USL / TCSL (Đề xuất | DSML chuyên biệt miền + LTS   | Đầy đủ bước, kiểu checkpoint,    |
| của Luận án)        | Operational Semantics + OCL   | dữ liệu cụ thể & trạng thái snapshot|
+---------------------+-------------------------------+----------------------------------+
  1. Nhánh tiếp cận dựa trên Ngôn ngữ mô hình hóa chuyên biệt miền (DSML):
    • Nghiên cứu của Escalona et al. [16, 23] trong phương pháp NDT (Navigational Development Techniques) sử dụng DSL để mô hình hóa yêu cầu web nhưng hoàn toàn bỏ ngỏ bài toán sinh dữ liệu kiểm thử biên.
    • Nhóm nghiên cứu ReDSeeDS (Smialek et al. [63, 65]) phát triển ngôn ngữ RSL (Requirements Specification Language) và ngôn ngữ kiểm thử TSL (Test Specification Language). Mặc dù RSL hỗ trợ phát triển hướng mô hình, thông tin trong RSL không đủ độ chi tiết để bộ sinh sinh ra giá trị kiểm thử cụ thể; ngôn ngữ TSL chỉ dừng lại ở việc đặc tả các điều kiện bằng lời thay vì giá trị gán thực tế.
    • Ngôn ngữ SelabReq [59] tích hợp tốt việc sinh biểu đồ lớp và biểu đồ tương tác nhưng không hỗ trợ bất kỳ cơ chế sinh ca kiểm thử nào.

Luận án của Chu Thị Minh Huệ định vị chính xác khoảng trống này bằng cách đề xuất bộ đôi ngôn ngữ chuyên biệt miền USL (Use Case Specification Language) và TCSL (Test Case Specification Language), kết hợp với kỹ thuật chuyển đổi mô hình M2M và công cụ giải ràng buộc OCL, tạo ra bước tiến vượt bậc: lần đầu tiên đưa quy trình sinh kiểm thử từ ca sử dụng đạt tới mức độ cụ thể hóa toàn diện (đầy đủ bước thực hiện, hành động, đối tượng giao diện, loại điểm kiểm tra checkpoint, dữ liệu đầu vào cụ thể và trạng thái cơ sở dữ liệu nội tại).

Đóng góp lý thuyết và khung phân tích

Đóng góp cho lý thuyết

Luận án đã mở rộng lý thuyết Kỹ nghệ phần mềm hướng mô hình (MDE) của Schmidt [62] và khung lý thuyết Kiểm thử dựa trên mô hình (MBT) của Utting & Legeard [56] thông qua ba trụ cột lý thuyết:

  1. Thiết lập Hình thức hóa Ngữ nghĩa cho Đặc tả Ca sử dụng (Formal Operational Semantics for Use Cases): Vượt qua hạn chế của lý thuyết ca sử dụng bán hình thức do Ivar Jacobson [27] khởi xướng, luận án xây dựng ánh xạ hình thức từ mô hình USL sang Hệ thống chuyển trạng thái được gán nhãn LTS: $$\mathcal{M}_{LTS} = (S, S_0, L, T)$$ Trong đó:

    • $S$: Tập hợp hữu hạn các trạng thái của ca sử dụng (bao gồm trạng thái bắt đầu $S_0$, trạng thái chờ người dùng nhập liệu, trạng thái xử lý logic của hệ thống, và trạng thái kết thúc).
    • $L$: Tập các nhãn hành động phân biệt rõ ràng: hành động của tác nhân ($Act_{actor}$), hành động của hệ thống ($Act_{system}$), và các điều kiện gác ($Guard$).
    • $T \subseteq S \times L \times S$: Quan hệ chuyển trạng thái xác định tính tất định và khả năng duyệt vét cạn không gian trạng thái.

  2. Khung lý thuyết Siêu mô hình hóa Đa tầng (Multi-level Metamodeling Architecture): Dựa trên chuẩn Meta-Object Facility (MOF) của OMG, luận án định nghĩa siêu mô hình trừu tượng cho USL và TCSL với hệ thống phân loại kiểu (type system) chặt chẽ. Cú pháp trừu tượng của USL phân tách rõ luồng sự kiện chính (BasicFlow), luồng phụ (AlternateFlow), luồng ngoại lệ (ExceptionFlow), các bước tương tác (Step), đối tượng giao diện (UIElement), cùng các biểu thức OCL biểu diễn tiền điều kiện (PreCondition), hậu điều kiện (PostCondition) và điều kiện rẽ nhánh (GuardCondition).

  3. Lý thuyết Chuyển đổi Mô hình Tích hợp Giải ràng buộc Khái niệm (Conceptual-Aware Model Transformation): Luận án chứng minh mệnh đề lý thuyết: "Một ca kiểm thử chức năng hoàn chỉnh ở mức hệ thống chỉ có thể được sinh ra một cách xác định khi và chỉ khi có sự kết hợp đồng thời giữa mô hình hành vi ca sử dụng (Behavioral Model - USL) và mô hình cấu trúc khái niệm miền (Domain Conceptual Model) thông qua cơ chế giải hệ ràng buộc bất biến (Invariants) và điều kiện gác (Guards)".

+-----------------------------------------------------------------------------------+
|                        KHUNG PHÂN TÍCH VÀ KIẾN TRÚC CHUYỂN ĐỔI                    |
+-----------------------------------------------------------------------------------+
|                                                                                   |
|   +-----------------------+              +------------------------------------+   |
|   |  Mô hình USL (Hành vi)|              | Mô hình Khái niệm Miền (Biểu đồ lớp|   |
|   |  - Basic / Alt Flows  |              | Entity + Ràng buộc OCL Invariants) |   |
|   +-----------+-----------+              +-----------------+------------------+   |
|               |                                            |                      |
|               +--------------------+  +--------------------+                      |
|                                    |  |                                           |
|                                    v  v                                           |
|                        +---------------------------+                              |
|                        | Phương pháp USLTG         |                              |
|                        | 1. Sinh kịch bản (APC)    |                              |
|                        | 2. Phân tích điều kiện gác|                              |
|                        | 3. Sinh dữ liệu qua USE   |                              |
|                        +-------------+-------------+                              |
|                                      |                                            |
|                                      v                                            |
|                        +---------------------------+                              |
|                        | Mô hình TCSL (Ca kiểm thử)|                              |
|                        | - TestSteps & Actions     |                              |
|                        | - Checkpoint Types        |                              |
|                        | - Input Data & Snapshots  |                              |
|                        +-------------+-------------+                              |
|                                      |                                            |
|                                      v                                            |
|                        +---------------------------+                              |
|                        | Bộ sinh mã Acceleo (M2T)  |                              |
|                        +-------------+-------------+                              |
|                                      |                                            |
|                        +-------------+-------------+                              |
|                        |                           |                              |
|                        v                           v                              |
|               +------------------+       +-------------------+                    |
|               | File XML / TCSL  |       | Tài liệu TUCD     |                    |
|               | (Tập lệnh KDTF)  |       | (Đặc tả theo mẫu) |                    |
|               +------------------+       +-------------------+                    |
+-----------------------------------------------------------------------------------+

Khung phân tích độc đáo

Khung phân tích của luận án kết hợp 3 lý thuyết nền tảng:

  • Lý thuyết Ngôn ngữ chuyên biệt miền (DSM Theory [9, 62]): Tối ưu hóa mức độ trừu tượng, thu hẹp khoảng cách ngữ nghĩa giữa tài liệu yêu cầu và mã kiểm thử.
  • Lý thuyết Bao phủ Kiểm thử Đồ thị (Graph-based Coverage Theory [39, 41]): Mở rộng tiêu chí phủ đường cơ bản (Basic Path Coverage) thành tiêu chí phủ đường hoạt động (Activity Path Coverage), cho phép kiểm thử toàn diện các cấu trúc lặp while-do (0 và 1 lần lặp), do-while (1 và 2 lần lặp), và tích hợp hành động song song (Fork/Join).
  • Lý thuyết Giải mô hình dựa trên Ràng buộc (Constraint Satisfaction & Snapshot Generation [18]): Sử dụng công cụ USE để giải các biểu thức OCL, tự động sinh ra biểu đồ đối tượng trạng thái trước ($OM_{partial}$) và trạng thái đầy đủ ($OM_{full}$) của hệ thống.

Điều kiện biên (Boundary Conditions): Phương pháp áp dụng tối ưu cho các hệ thống phần mềm hướng thông tin (information systems), xử lý giao dịch nghiệp vụ (business transaction systems) có mô hình dữ liệu quan hệ và hành vi chức năng được đặc tả tường minh qua ca sử dụng. Không áp dụng cho các hệ thống thời gian thực cứng (hard real-time systems) hoặc hệ thống xử lý song song phân tán phụ thuộc chặt vào độ trễ mạng.

Phương pháp nghiên cứu tiên tiến

Thiết kế nghiên cứu

Nghiên cứu tuân thủ thế giới quan thực chứng khoa học (Positivism) kết hợp với Phương pháp luận Khoa học Thiết kế (Design Science Research Methodology – DSRM) chuẩn mực trong Kỹ nghệ phần mềm. Thiết kế nghiên cứu đa tầng (Multi-level Design) kết hợp chặt chẽ giữa:

  1. Nghiên cứu lý thuyết và kỹ nghệ mô hình (Formal modeling, Metamodeling, Semantics mapping).
  2. Phát triển công cụ phần mềm (Tool implementation on Eclipse Platform).
  3. Đánh giá thực nghiệm so sánh đối chuẩn (Benchmarking and Comparative Empirical Evaluation).

Quy trình nghiên cứu rigorous

Quy trình nghiên cứu được tiến hành qua 4 giai đoạn nghiêm ngặt:

+-----------------------------------------------------------------------------------+
|                            QUY TRÌNH NGHIÊN CỨU 4 PHA                             |
+-----------------------------------------------------------------------------------+
|  [Pha 1: Khảo sát & Đặc tả Miền]                                                 |
|  - Trích xuất khái niệm miền ca sử dụng & ca kiểm thử                             |
|  - Thiết kế siêu mô hình USL & TCSL trên Eclipse EMF                              |
|  - Định nghĩa 15+ luật hợp lệ OCL (Well-formedness Rules)                         |
+-----------------------------------------------------------------------------------+
                                          |
                                          v
+-----------------------------------------------------------------------------------+
|  [Pha 2: Thiết kế Thuật toán USLTG]                                               |
|  - Thủ tục GenerateScenarios: Duyệt cây hành vi, trích xuất đường hoạt động       |
|  - Thuật toán GenTestInputData: Tích hợp công cụ USE giải OCL constraints         |
|  - Thuật toán GenTCSLModel: Ánh xạ phần tử sang siêu mô hình TCSL                 |
+-----------------------------------------------------------------------------------+
                                          |
                                          v
+-----------------------------------------------------------------------------------+
|  [Pha 3: Hiện thực hóa Bộ công cụ USL Tool]                                      |
|  - Trình soạn thảo đồ họa USL Editor (Eclipse GMF)                                |
|  - Bộ chuyển đổi M2M (ATL Engine) & M2T (Acceleo Engine)                          |
|  - Mô-đun tích hợp sinh tài liệu mẫu USL2TUCD và tệp XML đặc tả kiểm thử          |
+-----------------------------------------------------------------------------------+
                                          |
                                          v
+-----------------------------------------------------------------------------------+
|  [Pha 4: Thực nghiệm & Đánh giá Đối chuẩn]                                       |
|  - Áp dụng trên Case studies: ATM Withdraw, Library Lend Book, Course Registration|
|  - Đối chuẩn so sánh với RSL/TSL [65], RUCM [58], SelabReq [59], NDT [23]         |
|  - Đánh giá độ phức tạp Cyclomatic V(G) và độ bao phủ lỗi                         |
+-----------------------------------------------------------------------------------+

Độ tin cậy (Reliability) và Tính hợp lệ cấu trúc (Construct Validity) được đảm bảo tuyệt đối nhờ việc kiểm chứng tự động toàn bộ mô hình thông qua OCL Invariant Checker trên Eclipse và giải thuật toán học hình thức trên công cụ USE, loại bỏ hoàn toàn sự can thiệp chủ quan của con người trong quá trình sinh ca kiểm thử.

Data và phân tích

Dữ liệu phân tích bao gồm cấu trúc ca sử dụng và các tập ràng buộc logic từ các bài toán chuẩn:

  1. Ca sử dụng Rút tiền ATM (Withdraw): Bao gồm 1 luồng chính (10 bước tương tác), 5 luồng rẽ nhánh thay thế (sai mã PIN, số tiền không là bội số của 50.000 VNĐ, số dư không đủ, vượt hạn mức ngày, số tiền vượt quá số dư tối thiểu).
  2. Ca sử dụng Mượn sách (Lend Book): Bao gồm luồng chính (8 bước), 3 luồng thay thế (thẻ đọc giả hết hạn, sách đã có người mượn, độc giả đang giữ sách quá hạn).

Thuật toán cốt lõi và Công nghệ triển khai:

  • Thuật toán trích xuất kịch bản (GenerateScenarios): Áp dụng thuật toán duyệt đồ thị theo chiều sâu (DFS) có kiểm soát số lần lặp $k \le 2$ để đạt tiêu chí Phủ đường hoạt động (Activity Path Coverage). Độ phức tạp Cyclomatic của đồ thị được tính toán chính xác: $$V(G) = E - N + 2 = P + 1$$ (với $E$ là số cạnh, $N$ là số nút, $P$ là số điểm quyết định nhị phân) [33].
  • Thuật toán sinh dữ liệu kiểm thử (GenTestInputData): Trích xuất điều kiện tiền đề ($PreCondition$), điều kiện gác ($Guard$), kết hợp với tệp cấu hình $CONF$ và mô hình lớp $CM$, chuyển đổi thành kịch bản kiểm tra bất biến trong công cụ USE để sinh ra thể hiện cụ thể của các đối tượng $EV$ (Evaluation Objects) và giá trị biến nhập liệu.
  • Công nghệ triển khai: Ngôn ngữ Java, nền tảng Eclipse Modeling Framework (EMF), Graphical Modeling Framework (GMF), ATLAS Transformation Language (ATL), và Acceleo M2T Engine [22, 32].

Phát hiện đột phá và implications

Những phát hiện then chốt

  1. Khả năng tự động hóa đồng thời 100% kịch bản kiểm thử và dữ liệu kiểm thử cụ thể: Khác với nghiên cứu của Smialek et al. [65] trên ngôn ngữ TSL (chỉ đưa ra các mô tả điều kiện trừu tượng như "Invalid PIN"), phương pháp USLTG sinh ra chính xác bộ giá trị dữ liệu cụ thể (ví dụ: EnteredPIN = "1234", AccountBalance = 5.000.000, WithdrawAmount = 2.000.000) cùng trạng thái bảng cơ sở dữ liệu đối tượng Account tương ứng.
+----------------------------------------------------------------------------------------------------+
| TRÍCH XUẤT SO SÁNH CA KIỂM THỬ THỰC NGHIỆM: CA SỬ DỤNG RÚT TIỀN ATM (WITHDRAW)                     |
+-----+-------+------------------------+-------------------+--------------------+--------------------+
| TID | SID   | Bước tương tác         | Dữ liệu đầu vào   | Loại Checkpoint    | Kết quả mong đợi   |
+-----+-------+------------------------+-------------------+--------------------+--------------------+
| T01 | SC_01 | 1. Đưa thẻ vào đầu đọc | CardID="C001"     | UI State Check     | Giao diện nhập PIN |
|     | (Main)| 2. Nhập mã PIN         | PIN="1234" (Đúng) | Logic State Check  | Menu chọn giao dịch|
|     |       | 3. Chọn Rút tiền       | Option="Withdraw" | UI State Check     | Màn hình nhập tiền |
|     |       | 4. Nhập số tiền        | Amount=500.000    | Internal DB State  | Nhả tiền, in bill, |
|     |       | 5. Nhận tiền & thẻ     | Action="Confirm"  | Balance Check      | Balance=4.500.000  |
+-----+-------+------------------------+-------------------+--------------------+--------------------+
| T02 | SC_02 | 1. Đưa thẻ vào đầu đọc | CardID="C001"     | UI State Check     | Giao diện nhập PIN |
|     | (Alt) | 2. Nhập mã PIN sai     | PIN="9999" (Sai)  | Warning Checkpoint | Thông báo: "Mã PIN |
|     |       |                        |                   |                    | sai, nhập lại"     |
+-----+-------+------------------------+-------------------+--------------------+--------------------+
| T03 | SC_03 | 4. Nhập số tiền không  | Amount=125.000    | Validation Check   | Báo lỗi: "Số tiền  |
|     | (Alt) | phải bội số 50.000     |                   |                    | phải là bội 50k"   |
+-----+-------+------------------------+-------------------+--------------------+--------------------+
| T04 | SC_04 | 4. Số tiền rút vượt quá| Amount=10.000.000 | Balance Guard Check| Báo lỗi: "Số dư    |
|     | (Alt) | số dư tài khoản        | Balance=2.000.000 |                    | không đủ thực hiện"|
+-----+-------+------------------------+-------------------+--------------------+--------------------+

  1. Phát hiện và bao phủ toàn diện 3 lớp lỗi nghiêm trọng trong biểu đồ hoạt động: Thực nghiệm chứng minh phương pháp USLTG bao phủ triệt để:

    • Lỗi điểm quyết định (Decision errors): Đảm bảo mọi nhánh True/False của điều kiện gác đều có ít nhất một ca kiểm thử kích hoạt.
    • Lỗi vòng lặp (Loop errors): Với cấu trúc while-do và do-while, phương pháp sinh đầy đủ ca kiểm thử cho biên ranh giới $k=0$, $k=1$ và $k=2$ lần lặp, phát hiện các lỗi sai lệch điều kiện thoát vòng lặp.
    • Lỗi đồng bộ hóa (Synchronization errors): Duy trì chính xác quan hệ thứ tự ưu tiên của các nhánh hành động đồng thời (Fork/Join) thông qua cơ chế duyệt theo bề rộng (BFS traversal) [39].

  2. Tính đầy đủ vượt trội của Siêu mô hình TCSL: So với chuẩn kiểm thử hướng từ khóa (Keyword-Driven Testing Framework – KDTF), TCSL định nghĩa cấu trúc 6 chiều hoàn chỉnh: (1) StepIndex, (2) TestStepType, (3) Action & TargetUIElement, (4) CheckpointType, (5) ConcreteInputData & ExpectedOutput, và (6) SystemSnapshotState (trạng thái đối tượng trước và sau kiểm thử).

  3. Tích hợp hai chiều hoàn hảo trong MDE: Mô hình USL không chỉ dùng để sinh kiểm thử mà còn được chuyển đổi tự động ngược lại thành tài liệu đặc tả ca sử dụng theo mẫu ngôn ngữ tự nhiên ($USL2TUCD$) thông qua Acceleo M2T, phục vụ công tác nghiệm thu và giao tiếp với khách hàng phi kỹ thuật.

Implications đa chiều

  • Về mặt Lý thuyết: Chứng minh tính hiệu quả của việc kết hợp mô hình hóa chuyên biệt miền với ngữ nghĩa hình thức LTS trong việc loại bỏ sự mơ hồ của tài liệu yêu cầu.
  • Về mặt Phương pháp luận: Cung cấp quy trình mẫu (pipeline) khép kín từ mô hình hóa yêu cầu, giải ràng buộc tự động OCL, đến sinh đặc tả kiểm thử XML chuẩn hóa cho kỹ nghệ phần mềm.
  • Về mặt Thực tiễn Công nghiệp: Cắt giảm 70-80% thời gian thiết kế ca kiểm thử thủ công, loại bỏ sai sót của con người, và cho phép tự động cập nhật bộ kiểm thử hồi quy ngay khi mô hình USL thay đổi.
  • Về mặt Chính sách & Chuẩn hóa: Đề xuất hướng tiếp cận chuẩn hóa cho các doanh nghiệp gia công phần mềm trong việc áp dụng mô hình hóa chuyên biệt miền vào quy trình kiểm toán chất lượng phần mềm (CMMI Level 3-5).

Limitations và Future Research

Luận án thẳng thắn thừa nhận các giới hạn kỹ thuật:

  1. Sự phụ thuộc vào độ chính xác của Mô hình Lớp Khái niệm miền: Nếu biểu đồ lớp khái niệm hoặc các ràng buộc OCL định nghĩa ban đầu bị thiếu sót, bộ giải USE sẽ không thể sinh ra các snapshot trạng thái tương thích.
  2. Không gian bùng nổ tổ hợp ràng buộc phức tạp (Combinatorial Explosion): Khi số lượng điều kiện gác và biến đầu vào tăng theo cấp số nhân với các biểu thức phi tuyến tính, thời gian giải OCL solver sẽ tăng cao.
  3. Phạm vi kiểm thử chức năng: Luận án tập trung chuyên sâu vào kiểm thử chức năng mức hệ thống (Functional System Testing), chưa mở rộng sang kiểm thử phi chức năng (hiệu năng, tải, bảo mật).

Chương trình nghiên cứu tương lai (Future Research Agenda):

  • Mở rộng ngôn ngữ USL để mô hình hóa và sinh kiểm thử cho các yêu cầu phi chức năng (Non-functional requirements như độ trễ, thông lượng).
  • Tích hợp các bộ giải ràng buộc SMT tiên tiến (như Z3 Solver) nhằm tăng tốc độ giải các biểu thức toán học phức tạp.
  • Tự động hóa hoàn toàn pha 3: Sinh mã kiểm thử thực thi (executable test scripts) trực tiếp cho các framework như Selenium WebDriver, Appium, và Robot Framework từ mô hình TCSL.

Tác động và ảnh hưởng

Nghiên cứu của tác giả Chu Thị Minh Huệ tạo nên những ảnh hưởng sâu rộng:

  • Tác động Học thuật (Academic Impact): Đóng góp các bài báo công bố trên các tạp chí và kỷ yếu hội thảo uy tín (như Chuyên san Các công trình Nghiên cứu, Phát triển và Ứng dụng CNTT-TT; Hội thảo Quốc gia SoICT, FAIR), mở ra hướng nghiên cứu kết hợp DSM và OCL Solver trong kiểm thử phần mềm tại Việt Nam.
  • Chuyển đổi Công nghiệp (Industry Transformation): Cung cấp công cụ và phương pháp luận trực tiếp cho các công ty phần mềm, giúp chuyển đổi từ quy trình kiểm thử thủ công lạc hậu sang quy trình Kỹ nghệ phần mềm hướng mô hình hóa (MDE), tối ưu hóa chi phí sản xuất phần mềm.
  • Ý nghĩa Xã hội: Góp phần nâng cao độ tin cậy và chất lượng của các hệ thống thông tin trọng yếu quốc gia (ngân hàng số, chính phủ điện tử, y tế thông minh), hạn chế các sự cố phần mềm gây thiệt hại kinh tế.

Đối tượng hưởng lợi

  • Nghiên cứu sinh & Giới Học thuật (Doctoral & Senior Researchers): Tiếp cận một khung phân tích hình thức hoàn chỉnh về ngữ nghĩa LTS cho ca sử dụng và phương pháp giải ràng buộc OCL trong MDE.
  • Kỹ sư Trưởng & Chuyên gia Kiểm thử Phần mềm (QA/QC Leads & Test Architects): Sở hữu giải pháp tự động hóa sinh bộ kiểm thử với độ bao phủ cao, giảm thiểu chi phí bảo trì test suite trong các dự án Agile/DevOps.
  • Chuyên viên Phân tích Nghiệp vụ (Business Analysts - BA): Sử dụng ngôn ngữ trực quan USL để đặc tả chính xác yêu cầu khách hàng mà không cần kỹ năng lập trình phức tạp.
  • Nhà Quản lý Dự án Phần mềm (Software Project Managers): Rút ngắn chu kỳ phát hành sản phẩm (Time-to-Market), kiểm soát chặt chẽ chất lượng theo mô hình chữ V chuẩn quốc tế [50].

Câu hỏi chuyên sâu

1. Đóng góp lý thuyết độc đáo nhất của luận án là gì và đã mở rộng lý thuyết nào?

Đóng góp độc đáo nhất là việc thiết lập Ngữ nghĩa thực thi hình thức dựa trên Hệ thống chuyển trạng thái được gán nhãn (LTS Operational Semantics) cho ngôn ngữ đặc tả ca sử dụng USL, mở rộng lý thuyết Mô hình hóa Ca sử dụng của Ivar Jacobson [27] và Kỹ nghệ hướng mô hình (MDD) của Schmidt [62]. Bằng cách này, mô hình ca sử dụng không còn là một tài liệu văn bản mơ hồ mà trở thành một mô hình tính toán hình thức có khả năng chuyển đổi toán học chính xác sang mô hình kiểm thử TCSL.

2. Đổi mới phương pháp luận của luận án vượt trội hơn các nghiên cứu quốc tế trước đây như thế nào?

So với RUCM của Yue et al. [73] (dựa trên NLP và ngôn ngữ tự nhiên bị giới hạn) và RSL/TSL của Smialek et al. [65] (dựa trên ReDSeeDS), phương pháp USLTG vượt trội nhờ:

  • Tự động hóa sinh dữ liệu kiểm thử cụ thể (concrete values) và trạng thái hệ thống bên trong ($OM_{full}$) thông qua việc tích hợp bộ giải OCL trong USE tool, thay vì chỉ dừng lại ở kịch bản trừu tượng hoặc mô tả điều kiện định tính.
  • Đạt Tiêu chí phủ đường hoạt động (Activity Path Coverage) [39], kiểm soát trọn vẹn các lỗi vòng lặp (với $k \le 2$) và các hành động đồng thời song song, điều mà các nghiên cứu UML truyền thống [24, 67] không làm được.

3. Phát hiện thực nghiệm nào gây bất ngờ và có ý nghĩa nhất trong quá trình thực thi?

Phát hiện bất ngờ nhất là việc giải quyết bài toán Đồng bộ hóa dữ liệu trạng thái tiền điều kiện: Việc sinh dữ liệu kiểm thử không thể tách rời trạng thái nội tại của cơ sở dữ liệu. Luận án chứng minh rằng chỉ cần sử dụng mô hình USL kết hợp với biểu đồ lớp khái niệm miền, bộ sinh USLTG có thể tự động suy diễn và khởi tạo chính xác một Snapshot đối tượng hợp lệ trong cơ sở dữ liệu (ví dụ: tạo sẵn tài khoản Account có số dư thỏa mãn để kiểm thử ca rút tiền), loại bỏ hoàn toàn bước chuẩn bị dữ liệu thủ công phức tạp trong kiểm thử hệ thống.

4. Luận án có cung cấp giao thức tái lập thực nghiệm (Replication Protocol) hoàn chỉnh không?

Hoàn toàn đầy đủ. Luận án cung cấp chi tiết:

  • Siêu mô hình Ecore của USL và TCSL.
  • Toàn bộ các luật ràng buộc OCL hợp lệ (Well-formedness rules).
  • Mã giả của 3 thuật toán cốt lõi (GenerateScenarios, GenTestInputData, GenTCSLModel).
  • Quy tắc ánh xạ mô hình M2M và tập lệnh chuyển đổi M2T viết bằng ngôn ngữ Acceleo chuẩn hóa.

5. Định hướng nghiên cứu 10 năm tiếp theo được vạch ra như thế nào?

Lộ trình 10 năm tập trung vào 3 hướng đột phá:

  1. Nâng cấp bộ giải OCL bằng cách tích hợp các công cụ SMT Solver hiện đại (Z3, CVC4) để xử lý các ràng buộc dữ liệu lớn và phi tuyến.
  2. Mở rộng USL sang miền kiến trúc Microservices và hệ thống hướng dịch vụ (SOA/API testing).
  3. Ứng dụng trí tuệ nhân tạo (AI/LLMs) hỗ trợ tự động gợi ý và sinh mô hình USL từ tài liệu đặc tả thô ban đầu, tạo nên một chuỗi tự động hóa toàn diện từ ý tưởng đến kiểm thử phần mềm.

Kết luận

Luận án tiến sĩ của Chu Thị Minh Huệ đã giải quyết xuất sắc một trong những bài toán phức tạp và cấp thiết nhất của Kỹ nghệ phần mềm hiện đại với 5 đóng góp nền tảng:

  1. Đề xuất ngôn ngữ mô hình hóa chuyên biệt miền USL với cú pháp trừu tượng, cú pháp đồ họa trực quan và ngữ nghĩa hình thức LTS, biến ca sử dụng thành chế tác trung tâm trong MDD.
  2. Xây dựng ngôn ngữ TCSL đặc tả toàn diện ca kiểm thử chức năng mức hệ thống, bao gồm đầy đủ hành động, kiểu điểm kiểm tra, dữ liệu cụ thể và trạng thái hệ thống.
  3. Phát triển phương pháp USLTG tự động chuyển đổi từ mô hình USL và mô hình lớp khái niệm sang mô hình TCSL, đảm bảo tiêu chí phủ đường hoạt động và giải tự động các ràng buộc OCL.
  4. Hiện thực hóa Bộ công cụ hỗ trợ USL Tool trên nền tảng Eclipse (EMF, GMF, ATL, Acceleo), chứng minh tính khả thi qua các ca nghiên cứu thực tế (ATM, Library, Course Registration).
  5. Thiết lập cầu nối hoàn chỉnh giữa pha mô hình hóa yêu cầu và pha tự động hóa sinh dữ liệu kiểm thử, tạo tiền đề vững chắc cho việc ứng dụng Kỹ nghệ hướng mô hình (MDE) trong công nghiệp phần mềm.