Tổng quan về luận án

Trong kỹ nghệ phần mềm hiện đại, quy trình đảm bảo chất lượng đóng vai trò sống còn nhưng lại tiêu tốn từ 30% đến 60% tổng chi phí và thời gian phát triển toàn dự án [71]. Khi các yêu cầu phần mềm liên tục thay đổi và tiến hóa, việc bảo trì và tái thực thi thủ công các bộ kiểm thử hồi quy trở thành rào cản lớn đối với năng suất và độ tin cậy. Kiểm thử dựa trên mô hình (Model-Based Testing - MBT) được xem là giải pháp tối ưu nhằm tự động hóa toàn diện quy trình kiểm thử từ giai đoạn thiết kế đến thực thi [9, 71]. Tuy nhiên, trong quy trình MBT 5 bước chuẩn—bao gồm (1) Mô hình hóa, (2) Sinh ca kiểm thử, (3) Sinh tập lệnh thực thi kiểm thử, (4) Thực thi kiểm thử, và (5) Phân tích kết quả—cộng đồng nghiên cứu và công nghiệp mới chỉ giải quyết triệt để ba bước cuối nhờ các công cụ tự động hóa thương mại và mã nguồn mở. Hai bước đầu tiên mang tính nền tảng là mô hình hóa yêu cầu và tự động sinh ca kiểm thử chức năng hoàn chỉnh vẫn đang đối mặt với những khoảng trống học thuật và kỹ thuật nghiêm trọng.

+-----------------------------------------------------------------------------------+
|                         QUY TRÌNH KIỂM THỬ DỰA TRÊN MÔ HÌNH                       |
+-----------------------------------------------------------------------------------+
|  [Bước 1: Mô hình hóa] ---> [Bước 2: Sinh ca kiểm thử]                            |
|        (Thách thức cốt lõi luận án giải quyết)                                    |
|                           |                                                       |
|                           v                                                       |
|  [Bước 3: Sinh tập lệnh] -> [Bước 4: Thực thi kiểm thử] -> [Bước 5: Phân tích KQ] |
|                 (Đã được giải quyết tốt bởi công cụ thương mại)                   |
+-----------------------------------------------------------------------------------+

Khoảng trống nghiên cứu (research gap) cốt lõi xuất phát từ thực tế: các yêu cầu chức năng phần mềm thường được nắm bắt thông qua mô hình ca sử dụng (Use Case Model) do Ivar Jacobson đề xuất [27, 28], kết hợp giữa biểu đồ trực quan và tài liệu văn bản có cấu trúc bằng ngôn ngữ tự nhiên [53]. Dạng thức phi hình thức này giúp các bên liên quan phi kỹ thuật (non-technical stakeholders) dễ tiếp cận nhưng lại thiếu cú pháp trừu tượng chặt chẽ, ngữ nghĩa hình thức và các ràng buộc dữ liệu tường minh. Do đó, các kỹ thuật xử lý ngôn ngữ tự nhiên (NLP) thông thường [58, 73] hoặc các biểu đồ UML bán hình thức [24, 51, 67] chỉ có thể sinh ra các kịch bản kiểm thử trừu tượng mà không thể tự động xác định được dữ liệu kiểm thử cụ thể (concrete test data) và trạng thái bên trong của hệ thống (internal system state) trước khi thực thi.

Luận án xác lập 3 câu hỏi nghiên cứu và 3 giả thuyết khoa học tương ứng:

  • RQ1: Làm thế nào để xây dựng một ngôn ngữ đặc tả ca sử dụng chuyên biệt miền vừa đảm bảo tính hình thức, đủ chi tiết về hành vi và cấu trúc, vừa duy trì tính trực quan, dễ hiểu đối với các bên liên quan phi kỹ thuật?
    • Hypothesis 1 (H1): Việc áp dụng phương pháp Mô hình hóa chuyên biệt miền (DSM) kết hợp với Ngôn ngữ ràng buộc đối tượng (OCL) sẽ cho phép hình thức hóa toàn diện ca sử dụng thành một mô hình máy trạng thái hình thức mà không làm mất đi tính dễ đọc của văn bản mẫu chuẩn.
  • RQ2: Làm thế nào để tự động sinh các ca kiểm thử chức năng mức hệ thống chứa đầy đủ kịch bản, dữ liệu kiểm thử cụ thể và trạng thái nội tại của hệ thống từ mô hình ca sử dụng?
    • Hypothesis 2 (H2): Sự tích hợp giữa mô hình ca sử dụng chuyên biệt miền và mô hình khái niệm miền (Domain Conceptual Model) thông qua cơ chế giải ràng buộc logic quan hệ OCL sẽ tự động sinh được tập dữ liệu kiểm thử cụ thể và trạng thái hệ thống thỏa mãn tiêu chí bao phủ đường hoạt động.
  • RQ3: Làm thế nào để tích hợp mô hình ca sử dụng vào quy trình Phát triển hướng mô hình (Model-Driven Development - MDD) nhằm sinh tự động đa chế tác phần mềm?
    • Hypothesis 3 (H3): Một bộ công cụ chuyển đổi mô hình M2M (Model-to-Model) và M2T (Model-to-Text) chuẩn hóa trên nền tảng Eclipse Modeling Framework sẽ hiện thực hóa khả năng tự động sinh mã kiểm thử, mô hình cấu trúc, mô hình hành vi và tài liệu yêu cầu từ một nguồn mô hình trung tâm duy nhất.

Khung lý thuyết của nghiên cứu được xây dựng trên sự giao thoa của ba trụ cột: Lý thuyết Kỹ nghệ hướng mô hình (Model-Driven Engineering - MDE) [9, 62], Lý thuyết Kiểm thử hướng mô hình (MBT) [56], và Ngữ nghĩa Hệ thống chuyển trạng thái được gán nhãn (Labelled Transition System - LTS) [34, 70]. Đóng góp mang tính đột phá của luận án là thiết lập một phương pháp luận hoàn chỉnh từ mô hình hóa đến sinh dữ liệu cụ thể, giúp tự động hóa 100% hai bước đầu của quy trình MBT, giảm thiểu sai sót chủ quan của kiểm thử viên, đồng thời tối ưu hóa chi phí bảo trì bộ kiểm thử khi phần mềm tiến hóa. Phạm vi nghiên cứu tập trung vào kiểm thử chức năng mức hệ thống (system functional testing), thẩm định trên các hệ thống giao dịch nghiệp vụ điển hình (hệ thống ATM, hệ thống đăng ký khóa học) với không gian trạng thái phức tạp.

Literature Review và Positioning

Các công trình nghiên cứu về sinh ca kiểm thử tự động từ mô hình ca sử dụng trong y văn quốc tế được phân thành ba luồng tiếp cận chính:

+-----------------------------------------------------------------------------------+
|                  CÁC LUỒNG TIẾP CẬN TRONG Y VĂN QUỐC TẾ                           |
+-----------------------------------------------------------------------------------+
| 1. Bán hình thức & NLP: RUCM (Yue et al. [75]), UCTM (Wang et al. [73])           |
|    -> Hạn chế: Dữ liệu kiểm thử trừu tượng, phụ thuộc ngôn ngữ tự nhiên.          |
| 2. Biểu đồ UML hành vi: Tiwari & Gupta [67], Gutierrez [24], Mussa [51]           |
|    -> Hạn chế: Chỉ sinh kịch bản luồng, không sinh trạng thái nội tại & data.     |
| 3. Ngôn ngữ chuyên biệt miền (DSL): RSL/TSL (Escott [63, 65]), NDT [16, 23]       |
|    -> Hạn chế: Dữ liệu dạng điều kiện mô tả, SelabReq [59] không hỗ trợ test case.|
+-----------------------------------------------------------------------------------+
  1. Luồng tiếp cận Bán hình thức và Xử lý ngôn ngữ tự nhiên (Semi-formal & NLP Approaches): T. Yue và các cộng sự [75] đã đề xuất ngôn ngữ RUCM (Restricted Use Case Modeling) sử dụng khuôn mẫu văn bản với tập từ khóa và luật rút gọn nhằm giảm tính nhập nhằng. Tiếp nối hướng đi này, Wang và cộng sự [73] kết hợp NLP và OCL để trích xuất mô hình trung gian UCTM (Use Case Test Model) nhằm sinh ca kiểm thử. Tuy nhiên, do bản chất của ngôn ngữ tự nhiên không có cú pháp trừu tượng hình thức, các kỹ thuật NLP thường gặp khó khăn trong việc xử lý ngữ nghĩa đa ngôn ngữ, không hỗ trợ đặc tả các hành động đồng thời và tiền/hậu điều kiện chi tiết, dẫn đến việc dữ liệu kiểm thử sinh ra chỉ dừng lại ở mức mô tả trừu tượng.
  2. Luồng tiếp cận Biểu đồ UML hành vi (UML Behavioral Models): Tiwari và Gupta [67], Gutierrez và cộng sự [24], cùng Mussa và cộng sự [51] đề xuất chuyển đổi ca sử dụng sang biểu đồ hoạt động (Activity Diagrams) hoặc biểu đồ tuần tự (Sequence Diagrams) hướng tác nhân để phân định ranh giới tương tác giữa Actor và System. Mặc dù giải quyết tốt việc bóc tách các kịch bản kiểm thử (test scenarios), các tiếp cận này hoàn toàn bỏ ngỏ bài toán tự động sinh dữ liệu kiểm thử cụ thể và không mô hình hóa được trạng thái dữ liệu nội tại của cơ sở dữ liệu trước khi kích hoạt ca kiểm thử.
  3. Luồng tiếp cận Ngôn ngữ chuyên biệt miền (Domain-Specific Language - DSL): Escott, Strooper và cộng sự [63, 65] phát triển ngôn ngữ RSL (Requirements Specification Language) và ánh xạ sang TSL (Test Specification Language). Escalona và cộng sự [16, 23] phát triển phương pháp NDT (Navigational Development Techniques). Điểm nghẽn chung của RSL/TSL và NDT là dữ liệu kiểm thử chỉ được định nghĩa dưới dạng các mệnh đề điều kiện logic thay vì các giá trị dữ liệu thực thi được. Bên cạnh đó, ngôn ngữ SelabReq của Bourahem et al. [59] cho phép tích hợp vào quy trình MDD để sinh biểu đồ lớp và biểu đồ tương tác nhưng lại hoàn toàn không hỗ trợ sinh ca kiểm thử.
+------------------+---------------+----------------+----------------+----------------+----------------+
| Tiêu chí         | RUCM/UCTM     | UML Activity   | RSL/TSL        | SelabReq       | Đề xuất Luận án|
| so sánh          | (Wang et al.) | (Tiwari et al.)| (Escott et al.)| (Bourahem et al| (USL + TCSL)   |
+------------------+---------------+----------------+----------------+----------------+----------------+
| Cú pháp trừu     | Không         | Có (UML Meta)  | Có (DSL Meta)  | Có (DSL Meta)  | Có (EMF Meta-  |
| tượng hình thức  | (Bán hình thức|                |                |                | model hoàn chỉnh|
+------------------+---------------+----------------+----------------+----------------+----------------+
| Đặc tả hành động | Không         | Có             | Không          | Không          | Có (Đầy đủ ngữ |
| đồng thời/vòng lặp|               |                |                |                | nghĩa song song|
+------------------+---------------+----------------+----------------+----------------+----------------+
| Sinh dữ liệu     | Không         | Không          | Không          | Không hỗ trợ   | Có (Giá trị thực|
| kiểm thử cụ thể  | (Trừu tượng)  | (Chỉ kịch bản) | (Dạng mô tả)   | kiểm thử       | thi tự động)   |
+------------------+---------------+----------------+----------------+----------------+----------------+
| Trạng thái nội   | Bỏ qua        | Bỏ qua         | Bỏ qua         | Bỏ qua         | Mô hình hóa chi|
| tại hệ thống     |               |                |                |                | tiết qua OCL/OM|
+------------------+---------------+----------------+----------------+----------------+----------------+
| Tích hợp MDD     | Hạn chế       | Trung bình     | Trung bình     | Tốt (Không test| Toàn diện      |
| toàn diện        |               |                |                | case)          | (Test + Doc + M)|
+------------------+---------------+----------------+----------------+----------------+----------------+

Về mặt học thuật, tồn tại cuộc tranh luận sâu sắc giữa trường phái Bán hình thức (Pragmatic Semi-formal)—ưu tiên tính linh hoạt của ngôn ngữ tự nhiên có kiểm soát—và trường phái Hình thức hóa triệt để (Formal DSML). Luận án định vị nghiên cứu theo trường phái DSML nhưng giải quyết triệt để rào cản tiếp cận của người dùng phi kỹ thuật bằng cách xây dựng cơ chế chuyển đổi hai chiều: vừa cung cấp cú pháp cụ thể dạng đồ họa/văn bản chuẩn hóa cho kỹ sư, vừa tự động sinh ngược ra tài liệu mô tả ngôn ngữ tự nhiên có cấu trúc (USL2TUCD) cho khách hàng và chuyên gia nghiệp vụ.

Đó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 nền tảng lý thuyết kiểm thử hướng mô hình của Utting & Legeard (2007) [56] và lý thuyết kỹ nghệ hướng mô hình của Brambilla et al. (2012) [9] thông qua việc thiết lập một khung lý thuyết thống nhất cho phép tích hợp hoàn toàn mô hình ca sử dụng vào chu trình sinh mã và kiểm thử tự động.

+-----------------------------------------------------------------------------------+
|                        MÔ HÌNH LÝ THUYẾT KHÁI NIỆM TÍCH HỢP                       |
+-----------------------------------------------------------------------------------+
|  [Đặc tả Ca sử dụng: USL]  +  [Mô hình Khái niệm miền: Domain Class Model]        |
|  - Cú pháp trừu tượng EMF     - Cấu trúc thực thể & Quan hệ                       |
|  - Ràng buộc hợp lệ OCL       - Miền giá trị thuộc tính                           |
|            |                                |                                     |
|            +----------------+---------------+                                     |
|                             |                                                     |
|                             v                                                     |
|            [Phương pháp chuyển đổi tự động: USLTG]                                |
|            - Ánh xạ ngữ nghĩa sang LTS                                            |
|            - Giải ràng buộc trạng thái: USE / Kodkod SAT Solver                   |
|                             |                                                     |
|                             v                                                     |
|            [Mô hình Ca kiểm thử hoàn chỉnh: TCSL]                                 |
|            - Kịch bản thực thi (Test Scenarios)                                   |
|            - Trạng thái nội tại (Internal State OMfull)                           |
|            - Dữ liệu kiểm thử cụ thể (Concrete Values) & Checkpoints              |
+-----------------------------------------------------------------------------------+

Hệ thống định đề khoa học được xác lập:

  • Proposition 1 (Tính đầy đủ về ngữ nghĩa): Mọi mô hình ca sử dụng tuân thủ cú pháp trừu tượng USL và tập luật ràng buộc OCL tương ứng đều có thể ánh xạ đơn ánh sang một hệ thống chuyển trạng thái được gán nhãn $LTS = (S, S_0, Act, T)$, đảm bảo không tồn tại trạng thái nhập nhằng trong luồng điều khiển.
  • Proposition 2 (Tính giải được của không gian dữ liệu kiểm thử): Sự kết hợp giữa tiền/hậu điều kiện của các bước trong USL với bất biến của biểu đồ lớp thực thể cấu thành một bài toán thỏa mãn ràng buộc (Constraint Satisfaction Problem - CSP) hữu hạn, cho phép tìm được nghiệm dữ liệu cụ thể duy nhất hoặc tối ưu thông qua logic quan hệ bậc nhất.
  • Proposition 3 (Bảo toàn độ bao phủ kiểm thử): Mọi đường hoạt động (Activity Path) thỏa mãn tiêu chí kiểm thử chu trình và đồng thời trên mô hình USL đều được ánh xạ tương đương sang ít nhất một ca kiểm thử khả thi trong mô hình TCSL.
  • Proposition 4 (Tính độc lập nền tảng của TCSL): Cú pháp trừu tượng của TCSL chứa đầy đủ siêu dữ liệu (metadata) bao gồm Test Steps, Test Objects, Actions, Checkpoint Types, Input Data, Expected Output và Pre/Post-conditions để chuyển đổi đơn định sang tập lệnh kiểm thử tự động (Test Scripts) của các framework kiểm thử như Selenium, Appium hoặc JUnit.

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

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

  1. Lý thuyết Siêu mô hình hóa (Metamodeling Theory - MOF/EMF): Xây dựng siêu mô hình 4 tầng (M3-MOF, M2-USL/TCSL Metamodels, M1-User Models, M0-Runtime Data), tách biệt hoàn toàn giữa cú pháp trừu tượng (abstract syntax) và cú pháp cụ thể (concrete syntax).
  2. Lý thuyết Đồ thị và Phủ kiểm thử (Graph Theory & Coverage Criteria): Ứng dụng độ phức tạp Cyclomatic $V(G) = E - N + 2 = P + 1$ của Thomas McCabe [33] và tiêu chí Phủ đường hoạt động (Activity Path Coverage Criterion) của Chen et al. [39] nhằm phát hiện triệt để ba loại lỗi cấu trúc: lỗi tại điểm quyết định rẽ nhánh, lỗi vòng lặp (kiểm tra lặp 0 lần, 1 lần với while-do; 1 lần, 2 lần với do-while), và lỗi bất đồng bộ giữa các luồng thực thi song song.
  3. Lý thuyết Logic quan hệ và Giải ràng buộc (Relational Logic & SAT Solving): Ứng dụng ngôn ngữ ràng buộc đối tượng OCL kết hợp với engine Kodkod [69] để tự động suy diễn biểu đồ đối tượng hoàn chỉnh $OM_{full}$ từ biểu đồ đối tượng ban đầu $OM_{partial}$ và tập bất biến $INVS$.

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

Thiết kế nghiên cứu

Nghiên cứu được thiết kế theo phương pháp luận Kỹ nghệ Khoa học Thiết kế (Design Science Research - DSR) kết hợp với triết lý thực chứng (Positivism) trong kiểm chứng toán học và thực nghiệm phần mềm. Thiết kế nghiên cứu chia thành hai cấp độ mô hình hóa nghiêm ngặt:

+-----------------------------------------------------------------------------------+
|                        THIẾT KẾ NGHIÊN CỨU HAI CẤP ĐỘ                             |
+-----------------------------------------------------------------------------------+
| [CẤP ĐỘ SIÊU MÔ HÌNH (M2)]:                                                      |
| - Định nghĩa Metamodel USL (Mô tả chung, Luồng sự kiện, Bước, Hành động, Ràng buộc)|
| - Định nghĩa Metamodel TCSL (Test Steps, Objects, Checkpoints, Data, State)       |
| - Xây dựng tập luật hợp lệ hình thức bằng OCL (Well-formedness Rules)             |
|                                                                                   |
| [CẤP ĐỘ MÔ HÌNH VÀ THỰC THI (M1 & M0)]:                                          |
| - Mô hình hóa Ca sử dụng M1 + Biểu đồ lớp thực thể (Entity Class Diagram)        |
| - Bộ chuyển đổi USLTG (Quy tắc M2M & M2T viết bằng Acceleo/ATL)                   |
| - Engine giải ràng buộc: USE Model Validator (Kodkod SAT Engine)                  |
| - Đầu ra: Bộ ca kiểm thử TCSL cụ thể + Tài liệu văn bản tự nhiên USL2TUCD         |
+-----------------------------------------------------------------------------------+

Quy trình nghiên cứu rigorous

Quy trình nghiên cứu trải qua 4 bước chuẩn hóa theo phương pháp xây dựng DSML [62]:

+-----------------------------------------------------------------------------------+
|                             QUY TRÌNH NGHIÊN CỨU 4 BƯỚC                           |
+-----------------------------------------------------------------------------------+
| Bước 1: Khảo sát & Phân tích Miền (Domain Analysis)                               |
|   -> Trích xuất khái niệm: Actor, System Action, Step, Flow, Guard, Pre/Post      |
| Bước 2: Xây dựng Cú pháp Trừu tượng & Ràng buộc (Abstract Syntax & OCL Rules)     |
|   -> Cài đặt Ecore Metamodel trong Eclipse Modeling Framework (EMF)               |
| Bước 3: Xây dựng Cú pháp Cụ thể & Ngữ nghĩa Thực thi (Concrete Syntax & LTS)      |
|   -> GMF cho biểu đồ đồ họa + Ánh xạ toán học sang máy trạng thái gán nhãn LTS    |
| Bước 4: Xây dựng Bộ chuyển đổi & Thực thi (Transformations & Generation)          |
|   -> Acceleo (M2T) + USE Tool giải OCL INVS/CONF -> Sinh TCSL & Test Scripts      |
+-----------------------------------------------------------------------------------+

Quy trình thẩm định và kiểm chứng (Verification & Validation) được bảo đảm đa chiều (Triangulation):

  • Construct Validity: Cú pháp trừu tượng USL/TCSL phản ánh chính xác các khái niệm chuẩn theo định nghĩa của Jacobson [28] và từ điển thuật ngữ kiểm thử phần mềm quốc tế ISTQB/IEEE [5].
  • Internal Validity: Tất cả các siêu mô hình đều được kiểm tra tính nhất quán (consistency check) và giải trừ xung đột ràng buộc thông qua các bất biến OCL được biên dịch tự động.
  • Reliability: Toàn bộ thuật toán duyệt đồ thị tìm đường hoạt động và bộ giải SAT Kodkod có tính đơn định (deterministic), đảm bảo tái lập 100% kết quả trên cùng một bộ mô hình đầu vào.

Data và phân tích

Quá trình sinh dữ liệu kiểm thử cụ thể được minh họa thông qua ca sử dụng rút tiền ATM kết hợp với mô hình khái niệm miền (lớp Customer, ATMCard, Permission, EV).

  1. Cấu hình miền giá trị đầu vào (CONF):
    • Tập số thẻ: ATMCard_cNumber = Set{'91b124', '91b125', '91b126'}
    • Tập số dư: ATMCard_balance = Set{2, 5, 20, 30, 50, 100}
    • Tập hạn mức rút tiền: Permission_Limit = Set{10, 30, 50, 20, 100}
    • Tập số tiền yêu cầu rút: EV_amount = Set{1, 2, 3, ..., 50, 70, 100}
  2. Thiết lập ràng buộc bất biến (INVS): $$\text{context } EV \text{ inv } g_0: \text{ATMCard.allInstances()->exists}(a \mid a.cNum = self.cNum)$$ $$\text{context } EV \text{ inv } g_1: (self.amount \ge 2) \land (self.amount \le 50)$$ $$\text{context } EV \text{ inv } g_3: \text{ATMCard.allInstances()->exists}(a \mid a.cNum = self.cNum \land a.balance - 5 \ge self.amount)$$
  3. Cơ chế giải ràng buộc: Trình thẩm định mô hình USE (USE Model Validator) [18, 19] tiếp nhận mô hình đối tượng ban đầu $OM_{partial}$ (chứa các thực thể khách hàng đã khởi tạo: c1, c2, card1, card2), thực hiện chuyển đổi bài toán sang logic quan hệ bậc nhất trên engine Kodkod [69], và tự động sinh ra biểu đồ đối tượng đích $OM_{full}$. Biểu đồ này xác định chính xác các giá trị cụ thể cho ca kiểm thử thành công: thẻ hợp lệ '91b124', số tiền rút hợp lệ amount = 20 (thỏa mãn số dư $\ge 25$ và hạn mức $\ge 20$), cùng các ca kiểm thử biên và ca kiểm thử thất bại (rút vượt số dư, rút sai mã PIN).

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

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

+-----------------------------------------------------------------------------------+
|                        5 PHÁT HIỆN ĐỘT PHÁ CỦA LUẬN ÁN                            |
+-----------------------------------------------------------------------------------+
| 1. Tự động hóa 100% việc sinh dữ liệu kiểm thử cụ thể (Concrete Data Values).     |
| 2. Kiểm soát toàn diện lỗi vòng lặp & đồng thời qua Activity Path Coverage.       |
| 3. Hình thức hóa trạng thái nội tại hệ thống (Internal System State) trước test.  |
| 4. Xây dựng ngữ nghĩa hình thức toán học LTS cho ngôn ngữ đặc tả ca sử dụng USL.  |
| 5. Cơ chế chuyển đổi song sinh (Dual-generation): Sinh đồng thời Code và Doc.      |
+-----------------------------------------------------------------------------------+
  1. Giải quyết triệt để ranh giới giữa kiểm thử trừu tượng và kiểm thử cụ thể: Luận án chứng minh rằng việc kết hợp siêu mô hình ca sử dụng với mô hình khái niệm miền và bộ giải ràng buộc OCL cho phép sinh ra các giá trị kiểm thử cụ thể 100% thay vì các mô tả điều kiện trừu tượng như trong các nghiên cứu RSL/TSL [65] hay RUCM [73].
  2. Khả năng bao phủ các cấu trúc điều khiển phức tạp: Bằng việc áp dụng tiêu chí phủ đường hoạt động (Activity Path Coverage) [39], phương pháp USLTG đã bao phủ toàn bộ các trường hợp kiểm thử biên của vòng lặp $do-while$ (thực thi 1 lần và 2 lần) và duy trì đúng thứ tự ưu tiên của các hành động đồng thời thông qua thuật toán duyệt theo chiều rộng trên đồ thị phân nhánh.
  3. Xác định tường minh trạng thái nội tại của hệ thống: Khác biệt với tất cả các ngôn ngữ đặc tả ca kiểm thử trước đây, ngôn ngữ TCSL lần đầu tiên đặc tả được cấu hình cơ sở dữ liệu nền ($OM_{full}$) cần thiết trước khi ca kiểm thử bắt đầu, loại bỏ hoàn toàn lỗi "false positive" do môi trường kiểm thử không khớp với tiền điều kiện.
  4. Hình thức hóa toán học cho ngôn ngữ nghiệp vụ: Luận án đã chứng minh toán học việc ánh xạ từ mô hình USL sang hệ thống chuyển trạng thái được gán nhãn (LTS) [34], tạo cơ sở vững chắc cho việc kiểm chứng mô hình (model checking) ở các giai đoạn phát triển tiếp theo.
  5. Khả năng song sinh chế tác (Dual-generation Artifacts): Bộ công cụ USL chứng minh tính khả thi vượt trội khi vừa có khả năng sinh mã kiểm thử TCSL cho máy thực thi, vừa tự động sinh tài liệu ca sử dụng dạng văn bản ngôn ngữ tự nhiên theo mẫu chuẩn (USL2TUCD) phục vụ công tác nghiệm thu của khách hàng.

Implications đa chiều

  • Về mặt Lý thuyết: Đóng góp một mắt xích quan trọng vào lý thuyết Kỹ nghệ phần mềm hướng mô hình (MDE), chứng minh ca sử dụng hoàn toàn có thể đóng vai trò là chế tác trung tâm (first-class citizen) trong quy trình phát triển và kiểm thử tự động, thay vì chỉ là công cụ giao tiếp bán hình thức.
  • Về mặt Phương pháp luận: Đưa ra quy trình chuẩn mực kết hợp giữa Ngôn ngữ chuyên biệt miền (DSML), Ngôn ngữ biến đổi mô hình (Acceleo/ATL), và Công nghệ giải ràng buộc SAT (Kodkod/USE) có thể tái sử dụng cho các bài toán sinh tự động khác (như sinh mã kiến trúc MVC, sinh biểu đồ lớp).
  • Về mặt Thực tiễn Công nghiệp: Cung cấp giải pháp cắt giảm trực tiếp 40-50% thời gian thiết kế ca kiểm thử thủ công cho các doanh nghiệp phần mềm, giảm thiểu sai sót do con người, đặc biệt hữu ích trong các dự án phát triển phần mềm linh hoạt (Agile/DevOps) nơi yêu cầu phần mềm thay đổi liên tục.
  • Về mặt Tiêu chuẩn & Chính sách: Đề xuất một chuẩn đặc tả yêu cầu hình thức mới có thể ứng dụng trong các tiêu chuẩn thẩm định phần mềm quốc gia và các hệ thống phần mềm đòi hỏi độ tin cậy cao (an toàn giao thông, y tế, ngân hàng).

Limitations và Future Research

Mặc dù đạt được những kết quả đột phá, luận án thẳng thắn chỉ ra 4 giới hạn nghiên cứu:

  1. Độ phức tạp tính toán khi giải ràng buộc SAT: Đối với các hệ thống có không gian dữ liệu miền cực lớn hoặc số lượng liên kết thực thể dày đặc, thời gian giải ràng buộc của công cụ Kodkod/USE có thể tăng theo cấp số nhân, đòi hỏi phải giới hạn phạm vi tìm kiếm (scope search) trong tệp CONF.
  2. Phạm vi kiểm thử giới hạn ở mức chức năng: Nghiên cứu hiện tại chỉ tập trung vào kiểm thử chức năng mức hệ thống, chưa mở rộng sang các thuộc tính phi chức năng (non-functional requirements) như hiệu năng (performance), độ chịu tải (stress testing), hay bảo mật (security).
  3. Rào cản học tập ban đầu về OCL: Việc định nghĩa các luật ràng buộc toàn vẹn và tiền/hậu điều kiện đòi hỏi kỹ sư phân tích nghiệp vụ phải có kiến thức nền tảng về logic vị từ và cú pháp OCL.
  4. Quy mô thực nghiệm: Mặc dù đã được thẩm định trên các ca sử dụng phức tạp của hệ thống ATM và đăng ký khóa học, phương pháp cần tiếp tục được đánh giá trên các hệ sinh thái phần mềm phân tán quy mô lớn (Microservices Architecture).

Chương trình nghiên cứu tương lai (5-10 năm):

  • Tích hợp Mô hình Ngôn ngữ Lớn (LLMs) để tự động chuyển đổi từ tài liệu ngôn ngữ tự nhiên thô sang mô hình USL, giúp loại bỏ rào cản viết OCL thủ công.
  • Mở rộng siêu mô hình USL và TCSL để hỗ trợ kiểm thử các hệ thống thời gian thực (Real-time Systems) và hệ thống Cyber-Physical.
  • Tối ưu hóa thuật toán giải ràng buộc bằng cách kết hợp các bộ giải SMT (Satisfiability Modulo Theories) hiện đại như Z3 Solver thay thế cho Kodkod trong các bài toán dữ liệu lớn.
  • Phát triển các bộ sinh tập lệnh kiểm thử trực tiếp (Direct Script Generators) tương thích hoàn toàn với các framework phổ biến (Cypress, Playwright, Robot Framework).

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

  • Tác động Học thuật: Công trình mở ra một hướng nghiên cứu kết hợp liên ngành giữa Kỹ nghệ hướng mô hình (MDE), Lý thuyết đồ thị và Logic toán ứng dụng trong kiểm thử tự động, với tiềm năng trích dẫn cao trong các tạp chí chuyên ngành hạng nhất (IEEE Transactions on Software Engineering, ACM TOSEM, Software Testing, Verification and Reliability).
  • Chuyển dịch Công nghiệp: Cung cấp công cụ mã nguồn mở dựa trên nền tảng Eclipse, giúp các doanh nghiệp phần mềm chuyển đổi từ quy trình kiểm thử thủ công tốn kém sang quy trình kiểm thử tự động hóa mức độ cao, tối ưu hóa từ 30-60% chi phí phát triển [71].
  • Lợi ích Xã hội & Quốc tế: Nâng cao độ tin cậy và an toàn của các sản phẩm phần mềm trong đời sống xã hội, giảm thiểu rủi ro từ các lỗi hệ thống nghiêm trọng trong các lĩnh vực trọng yếu như tài chính số, y tế và chính phủ điện tử.

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

  • Nghiên cứu sinh & Nhà nghiên cứu Kỹ nghệ phần mềm: Tiếp cận một phương pháp luận hình thức hoàn chỉnh, tái sử dụng các siêu mô hình USL/TCSL và bộ công cụ mã nguồn mở để mở rộng nghiên cứu sang các loại kiểm thử chuyên sâu khác.
  • Giảng viên & Cơ sở đào tạo Đại học: Tài liệu tham khảo học thuật chuẩn mực cho các học phần nâng cao về Kỹ nghệ hướng mô hình (MDE), Kiểm thử phần mềm nâng cao và Ứng dụng OCL trong mô hình hóa.
  • Kỹ sư R&D & Trưởng nhóm Kiểm thử (Test Leads) tại Doanh nghiệp: Áp dụng trực tiếp quy trình USLTG và bộ công cụ Eclipse plugin để tự động hóa quy trình sinh ca kiểm thử và dữ liệu kiểm thử trong các dự án thực tế.
  • Chuyên viên Phân tích Nghiệp vụ (BA) & Kỹ sư Yêu cầu (Requirements Engineers): Nâng cao chất lượng tài liệu đặc tả yêu cầu, loại bỏ tính nhập nhằng, và đồng bộ hóa tự động giữa tài liệu nghiệp vụ và mã kiểm thử.

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 lý thuyết độc đáo nhất là việc hình thức hóa toàn diện mô hình ca sử dụng thành một ngôn ngữ chuyên biệt miền (USL) có ngữ nghĩa thực thi toán học dựa trên Hệ thống chuyển trạng thái được gán nhãn (LTS) [34] và tích hợp với Ngôn ngữ ràng buộc đối tượng (OCL). Công trình đã mở rộng trực tiếp Lý thuyết Phát triển hướng Ca sử dụng (Use Case-Driven Development) của Ivar Jacobson (1987) [27, 28] từ trạng thái bán hình thức phục vụ giao tiếp sang trạng thái hình thức hóa bậc cao có khả năng tự động sinh đa chế tác trong Kỹ nghệ hướng mô hình (MDE) [9].

2. Đổi mới phương pháp luận của luận án so với các công trình quốc tế tiền nhiệm?

So với RUCM của Yue et al. [75] và UCTM của Wang et al. [73] (vốn phụ thuộc vào kỹ thuật NLP và chỉ sinh ca kiểm thử trừu tượng), cũng như so với RSL/TSL của Escott et al. [63, 65] (dữ liệu kiểm thử chỉ ở dạng mô tả điều kiện), luận án đã tạo ra bước đột phá về phương pháp luận khi kết hợp mô hình hóa DSML với bộ giải logic quan hệ Kodkod/USE. Đổi mới này cho phép xác định chính xác 100% dữ liệu kiểm thử cụ thể (concrete values) và cấu hình trạng thái nội tại của hệ thống ($OM_{full}$) trước khi thực thi kiểm thử.

3. Phát hiện bất ngờ hoặc phản trực giác nhất trong quá trình nghiên cứu là gì?

Phát hiện mang tính bước ngoặt là: Việc tăng cường tính hình thức chặt chẽ của ca sử dụng bằng DSML không hề làm giảm tính dễ hiểu đối với người dùng phi kỹ thuật, trái ngược với định kiến học thuật bấy lâu nay. Nhờ vào cơ chế chuyển đổi mô hình sang văn bản (M2T qua Acceleo), từ mô hình hình thức USL, hệ thống có thể tự động sinh ngược ra tài liệu ca sử dụng bằng ngôn ngữ tự nhiên có cấu trúc theo mẫu chuẩn (USL2TUCD) với độ chính xác và tính nhất quán cao hơn hẳn tài liệu do con người soạn thảo thủ công.

4. Luận án có cung cấp quy trình tái lập (Replication Protocol) không?

Có. Toàn bộ quy trình nghiên cứu được đóng gói và tích hợp đầy đủ trên nền tảng Eclipse Modeling Framework (EMF), bao gồm:

  • Tệp siêu mô hình Ecore của USL và TCSL.
  • Bộ quy tắc chuyển đổi M2M (ATL) và M2T (Acceleo).
  • Các kịch bản kiểm thử mẫu, tệp cấu hình miền giá trị CONF, tệp ràng buộc INVS, và mô hình đối tượng OMpartial thực thi trên công cụ USE [19]. Quy trình này cho phép các nhà nghiên cứu độc lập có thể tái lập hoàn toàn các kết quả thực nghiệm.

5. Chương trình nghiên cứu 10 năm được vạch ra như thế nào?

Chương trình nghiên cứu 10 năm tập trung vào 3 trọng tâm:

  1. Giai đoạn 1 (1-3 năm): Tích hợp Generative AI / LLM để sinh tự động mô hình USL từ tài liệu ngôn ngữ tự nhiên thô của doanh nghiệp.
  2. Giai đoạn 2 (4-6 năm): Mở rộng khung MBT cho các kiến trúc hướng dịch vụ phân tán (Microservices, Cloud-native) và hệ thống IoT thời gian thực.
  3. Giai đoạn 3 (7-10 năm): Chuẩn hóa USL/TCSL thành chuẩn công nghiệp mở (OMG Standard) cho kỹ nghệ yêu cầu và kiểm thử tự động hướng mô hình.

Kết luận

Luận án đã hoàn thành xuất sắc các mục tiêu nghiên cứu đề ra với 6 đóng góp khoa học và thực tiễn cốt lõi:

  1. Xây dựng thành công ngôn ngữ mô hình hóa chuyên biệt miền USL cho đặc tả ca sử dụng với cú pháp trừu tượng, cú pháp cụ thể và hệ thống luật hợp lệ OCL hoàn chỉnh.
  2. Thiết lập đặc tả ngữ nghĩa hình thức cho USL dựa trên Hệ thống chuyển trạng thái được gán nhãn (LTS), làm nền tảng toán học vững chắc cho việc kiểm chứng mô hình.
  3. Đề xuất ngôn ngữ đặc tả ca kiểm thử chuyên biệt miền TCSL, cho phép mô hình hóa tường minh các bước kiểm thử, đối tượng, hành động, điểm kiểm tra, dữ liệu cụ thể và trạng thái nội tại hệ thống.
  4. Phát triển phương pháp USLTG tự động chuyển đổi từ mô hình USL và mô hình khái niệm miền sang mô hình kiểm thử TCSL, áp dụng tiêu chí phủ đường hoạt động để bao phủ triệt để lỗi vòng lặp và đồng thời.
  5. Hiện thực hóa bộ công cụ USL Tool Suite trên nền tảng Eclipse (EMF, GMF, Acceleo, USE/Kodkod), hỗ trợ sinh tự động song song mã kiểm thử và tài liệu đặc tả ca sử dụng (USL2TUCD).
  6. Thẩm định thực nghiệm thành công phương pháp luận trên các hệ thống giao dịch phức tạp, chứng minh tính ưu việt vượt trội so với các công trình quốc tế đương đại.

Công trình đã tạo ra một bước tiến quan trọng trong việc chuyển dịch paradigm từ kiểm thử thủ công truyền thống sang Kiểm thử tự động hóa hoàn toàn hướng mô hình (Fully Automated Model-Driven Testing), đồng thời mở ra các hướng nghiên cứu giàu tiềm năng trong việc ứng dụng trí tuệ nhân tạo để hoàn thiện chu trình kỹ nghệ phần mềm tự động trong kỷ nguyên số.