Tổng quan về luận án

Kỹ nghệ hướng mô hình (Model-Driven Engineering - MDE) đã xác lập một bước chuyển dịch căn bản trong kỹ nghệ phần mềm hiện đại, đặt các mô hình (models) và các bộ chuyển đổi mô hình (model transformations - MT) vào vị trí trung tâm của toàn bộ vòng đời phát triển. Đúng như khẳng định trong văn bản luận án: "Kỹ nghệ hướng mô hình (Model-Driven Engineering - MDE) đang trở thành một phương pháp phổ biến để phát triển các ứng dụng phần mềm quy mô lớn, phức tạp, trong đó các bộ chuyển đổi mô hình đóng vai trò then chốt để hiện thực hóa các tác vụ của quy trình phát triển." Tuy nhiên, việc đảm bảo chất lượng của các bộ chuyển đổi mô hình đối mặt với rào cản kỹ thuật nghiêm ngặt do tính phức tạp cú pháp, ngữ nghĩa đa tầng của ngôn ngữ mô hình hóa và tính chất không đơn định (non-deterministic) trong quá trình thực thi quy tắc chuyển.

Luận án tiến sĩ kỹ thuật phần mềm (mã số 9480103.01) của nghiên cứu sinh Nguyễn Thị Hạnh, thực hiện dưới sự hướng dẫn khoa học của PGS. Hồ Sĩ Đàm và TS. Đặng Đức Hạnh tại Trường Đại học Công nghệ – Đại học Quốc gia Hà Nội (2023), giải quyết triệt để bài toán này thông qua đề xuất công trình: "Khung hình thức hỗ trợ đảm bảo chất lượng chuyển đổi mô hình" (Formal Framework for Quality Assurance of Model Transformations).

Khoảng trống nghiên cứu (research gap) cốt lõi xuất phát từ việc các phương pháp kiểm thử hộp trắng phụ thuộc chặt vào ngôn ngữ cài đặt chuyên biệt miền (domain-specific transformation languages như ATL, QVTr, RTL) vốn phân mảnh và biến đổi liên tục, trong khi các phương pháp kiểm thử hộp đen hướng đặc tả hiện hành mới chỉ dừng lại ở việc biểu diễn cam kết hành vi rời rạc, thiếu vắng một khung lý thuyết hình thức thống nhất tích hợp đầy đủ cả cam kết kiểu, cam kết hành vi tĩnh và cam kết thể thức chuyển động.

Để giải quyết khoảng trống đó, luận án thiết lập hệ thống câu hỏi nghiên cứu (Research Questions - RQ) và giả thuyết khoa học (Hypotheses - H):

  • RQ1: Làm thế nào để xây dựng một ngôn ngữ đặc tả chuyển đổi mô hình dựa trên cam kết ở mức trừu tượng cao, độc lập với nền tảng cài đặt, trực quan nhưng sở hữu ngữ nghĩa hình thức toán học chặt chẽ?
  • RQ2: Cơ chế phân vùng không gian mô hình hóa và phân tích quan hệ phụ thuộc luật chuyển đổi có thể tự động hóa việc sinh các ca kiểm thử hộp đen đạt độ bao phủ tối ưu như thế nào?
  • RQ3: Làm thế nào để cấu trúc các hàm phán xét kiểm thử bộ phận (partial test oracles) nhằm kiểm chứng toàn diện các thuộc tính chất lượng chức năng bao gồm tính đúng đắn ngữ pháp, tính bảo toàn thông tin, tính đầy đủ, tính hội tụ và tính kết thúc?
  • H1: Việc tích hợp lý thuyết Văn phạm tam đồ thị (Triple Graph Grammars - TGG) vào ngôn ngữ đặc tả TC4MT cho phép mô hình hóa đồng thời cấu trúc tĩnh và động, làm cơ sở sinh tự động 100% các ràng buộc kiểm thử OCL.
  • H2: Chiến lược kết hợp phân vùng siêu mô hình và cam kết hành vi (kiểm thử khẳng định/phủ định) cùng phân tích chuỗi phụ thuộc luật chuyển cho phép phát hiện lỗi đột biến ngữ nghĩa vượt trội so với các phương pháp kiểm thử ngẫu nhiên hoặc kiểm thử cấu trúc đơn lẻ.

Khung lý thuyết của luận án tích hợp chặt chẽ: Kiến trúc hướng mô hình (Model Driven Architecture - MDA/MOF của OMG), Lý thuyết chuyển đổi đồ thị đại số (Algebraic Graph Transformation của Hartmut Ehrig et al., 2006), Văn phạm tam đồ thị (TGG của Andy Schürr, 1994) và Nguyên lý Thiết kế theo cam kết (Design by Contract của Bertrand Meyer, 1992). Phạm vi nghiên cứu tập trung vào các bộ chuyển đổi mô hình ngoại sinh từ mô hình sang mô hình (exogenous M2M), định hình phạm vi thực nghiệm trên các ca chuyển đổi chuẩn hóa (tiêu biểu là CD2RDBM - từ biểu đồ lớp UML sang lược đồ cơ sở dữ liệu quan hệ) với hàng trăm đột biến ngữ nghĩa được đánh giá định lượng.

Literature Review và Positioning

Nghiên cứu định vị bản thân tại giao lộ của ba dòng chảy học thuật lớn trong công nghệ phần mềm:

Dòng nghiên cứu thứ nhất tập trung vào việc hình thức hóa ngôn ngữ chuyển đổi mô hình. Kể từ khi Object Management Group chuẩn hóa MOF (2006) và QVT (2008), các ngôn ngữ như ATL (Jouault et al., 2008), QVTr/QVTc và RTL (Baudry et al., 2010) đã ra đời nhằm cung cấp cơ chế thực thi M2M. Tuy nhiên, các ngôn ngữ này phân hóa sâu sắc giữa cách tiếp cận khai báo/quan hệ và cách tiếp cận mệnh lệnh/thực thi, khiến việc kiểm thử hộp trắng bị cô lập trong từng môi trường thực thi cụ thể.

Dòng nghiên cứu thứ hai liên quan đến mô hình chất lượng chuyển đổi mô hình. Dựa trên mô hình chất lượng phần mềm kinh điển của Boehm (1978), Amstel et al. (2011) đã hệ thống hóa các thuộc tính chất lượng phi chức năng (understandability, modifiability, reusability, modularity). Tiếp đó, Hartmut et al. (2006) và Lukman et al. (2013) phân loại các thuộc tính chất lượng chức năng thiết yếu: tính đúng đắn cú pháp (syntactical correctness), tính bảo toàn ngữ nghĩa (semantic preservation gồm information & behavior preservation), tính đầy đủ (completeness), tính kết thúc (termination) và tính hội tụ (confluence).

Dòng nghiên cứu thứ ba là kiểm thử và kiểm chứng chuyển đổi mô hình. Các công trình kiểm chứng hình thức sử dụng Theorem Provers hoặc Model Checkers (như Calegari et al., Troya et al.) tuy đảm bảo tính toán học tuyệt đối nhưng gặp rào cản bùng nổ không gian trạng thái khi áp dụng vào các mô hình công nghiệp quy mô lớn. Ngược lại, các công trình kiểm thử hộp đen dựa trên phân vùng siêu mô hình (Fleurey et al., 2009; Sen et al., 2009) hoặc giải ràng buộc OCL/Alloy (Gogolla et al., 2007; Cabot et al., 2010) chỉ mới khai thác các khía cạnh đơn lẻ của siêu mô hình nguồn mà chưa gắn kết trực tiếp với cam kết hành vi và quy tắc chuyển đổi động.

Trong bức tranh tổng quan đó, tồn tại sự tranh luận học thuật rõ nét giữa hai trường phái xây dựng phán xét kiểm thử (test oracle):

  1. Trường phái Phán xét đầy đủ (Full Oracle): Sử dụng các công cụ so sánh mô hình (như Epsilon Comparison Language - ECL) để so khớp trực tiếp toàn bộ đồ thị mô hình đầu ra thực sự với mô hình kỳ vọng. Luận án chỉ ra điểm nghẽn lý thuyết cốt tử: "Thuật toán so sánh hai mô hình trong phán xét đầy đủ là trường hợp của đẳng cấu đồ thị, đây là một bài toán NP-Complete [31], đòi hỏi những kiến thức sâu sắc về ngữ nghĩa của ngôn ngữ mô hình hóa đích. Bên cạnh đó hầu hết ngữ nghĩa thực thi của các ngôn ngữ cài đặt chuyển đổi mô hình là không đơn định [23] dẫn tới khó khăn khi so sánh mô hình đầu ra thực sự."
  2. Trường phái Phán xét bộ phận (Partial Oracle): Được dẫn dắt bởi Lukman et al. (2013) và Selim et al. (2012), thẩm định tập thuộc tính mong đợi trên mô hình kết quả. Tuy nhiên, các nghiên cứu trước đây chưa chỉ ra được cơ chế suy diễn tự động các vị từ phán xét bộ phận từ một bản đặc tả hình thức đa cấp độ.

Luận án khẳng định vị thế tiên phong bằng cách kết nối TGG với kỹ thuật kiểm thử phân vùng tương đương và kiểm thử văn phạm, vượt lên hai nghiên cứu quốc tế điển hình: vượt qua hạn chế phụ thuộc công cụ thực thi của DSLTrans (Barroca et al., 2011) và giải quyết triệt để tính thiếu hụt cam kết thể thức trong mô hình kiểm thử của Fleurey et al. (2009).

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

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

Luận án đóng góp quan trọng cho lý thuyết Kỹ nghệ phần mềm hướng mô hình thông qua việc mở rộng và hợp nhất lý thuyết Văn phạm tam đồ thị (TGG) của Andy Schürr và nguyên lý Thiết kế theo cam kết (Design by Contract) của Bertrand Meyer vào không gian kiểm thử M2M. Cụ thể:

  1. Thiết lập mô hình phân tầng cam kết 4 cấp độ: Luận án mở rộng khái niệm cam kết phần mềm truyền thống thành cấu trúc phân cấp nghiêm ngặt cho chuyển đổi mô hình:
    • Cấp độ 1 (Cam kết kiểu - Type Contracts): Định nghĩa không gian dữ liệu hợp thức thông qua các siêu mô hình nguồn/đích được mô hình hóa thành các đồ thị kiểu thuộc tính hóa (Typed Attributed Graphs - TG).
    • Cấp độ 2 (Cam kết hành vi - Behavioral Contracts): Thiết lập các ràng buộc tiền điều kiện (Preconditions - Pre), hậu điều kiện (Postconditions - Post) và bất biến (Invariants - Inv) dưới dạng các mẫu đồ thị và biểu thức boolean OCL nhằm định vị chính xác không gian trạng thái hợp lệ và bất hợp lệ.
    • Cấp độ 3 (Cam kết thể thức - Step/Operational Contracts): Diễn đạt sự tiến hóa và ánh xạ đồng bộ giữa các phần tử mô hình nguồn - đích tại từng bước chuyển thông qua hệ thống luật tam đồ thị khai báo (Declarative Triple Graph Rules).
    • Cấp độ 4 (Cam kết thuộc tính chất lượng - Quality Property Contracts): Đảm bảo các chỉ tiêu toàn vẹn hệ thống (tính đúng cú pháp, bảo toàn thông tin, bảo toàn hành vi, tính hội tụ và tính kết thúc) dựa trên việc thỏa mãn đồng thời ba cấp độ cam kết nền tảng.
  2. Hình thức hóa ngôn ngữ đặc tả TC4MT (Test Cases for Model Transformations): Luận án luận giải nguyên lý thiết kế của TC4MT: "Ngôn ngữ TC4MT cho phép mô tả một cách có hệ thống các loại cam kết khác nhau như cam kết kiểu, cam kết hành vi và cam kết thể thức chuyển. Các cam kết được diễn đạt một cách trực quan bởi các mẫu đồ thị và luật chuyển tam đồ thị sử dụng cú pháp dạng sơ đồ lớp UML kết hợp các biểu thức ràng buộc OCL." Cú pháp trừu tượng và ngữ nghĩa hình thức của TC4MT tạo nền tảng vững chắc để chuyển đổi hai chiều mức cao (Higher-Order Transformations - HOTs) sang các ngôn ngữ PSM như QVTr, ATL, RTL.

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

Khung phân tích của luận án tích hợp ba trụ cột lý thuyết toán học và mô hình hóa:

  • Lý thuyết Đồ thị định kiểu và Cấu xạ tam đồ thị: Một tam đồ thị được định nghĩa hình thức bởi bộ ba $G = (G^S \xleftarrow{s_G} G^C \xrightarrow{t_G} G^T)$, trong đó $G^S$ là đồ thị nguồn, $G^T$ là đồ thị đích, $G^C$ là đồ thị tương ứng duy trì dấu vết ánh xạ (traceability), cùng hai cấu xạ đồ thị $s_G, t_G$. Cấu xạ tam đồ thị định kiểu $m = (m^S, m^C, m^T): G \to H$ bảo toàn cấu trúc phân loại của siêu mô hình tam đồ thị $TG$.
  • Lý thuyết Viết lại đồ thị đại số (Algebraic Graph Rewriting): Mỗi luật tam đồ thị khai báo $tr = (tr: L \to R, ac)$ xác định quy tắc ánh xạ bảo toàn cấu trúc từ tam đồ thị vế trái ($L$) sang vế phải ($R$), kèm điều kiện áp dụng bổ sung ($ac$). Các luật thực thi dẫn xuất (chuyển đổi tiến $tr_F$, chuyển đổi lùi $tr_B$, tích hợp $tr_I$) được tính toán tự động từ luật khai báo, loại bỏ tính mập mờ trong quá trình cài đặt.
  • Lý thuyết Ràng buộc logic bậc nhất (First-Order Logic Constraints): Tích hợp OCL chuẩn tắc để biểu diễn các điều kiện áp dụng phủ định (Negative Application Conditions - NAC), bất biến phủ định và các phân vùng biên giá trị.

Điều kiện biên (Boundary Conditions): Khung phân tích vận hành chuẩn xác trên mọi hệ thống chuyển đổi mô hình tuân thủ chuẩn MOF của OMG, áp dụng cho chuyển đổi mô hình ngoại sinh đơn hướng hoặc hai chiều, với giả định cấu trúc mô hình đầu vào có thể biểu diễn hữu hạn dưới dạng đồ thị định kiểu.

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

Thiết kế nghiên cứu

Luận án áp dụng lập trường triết học thực chứng kết hợp thuyết hiện thực phản biện (Critical Realism) trong kỹ nghệ phần mềm: hiện thực hóa các cấu trúc ngữ nghĩa trừu tượng thành các thực thể toán học có thể đo lường và kiểm chứng thực nghiệm. Thiết kế nghiên cứu đa tầng kết hợp phân tích tĩnh (Static Analysis) trên đặc tả với kiểm thử động (Dynamic Testing) trên môi trường thực thi:

[Đặc tả TC4MT (PIM)] 
       │
       ├──> (Nhánh 1) Phân tích Siêu mô hình & Cam kết Hành vi ──> Phân vùng Tương đương OCL ──> Kiểm thử Khẳng định/Phủ định
       │
       └──> (Nhánh 2) Phân tích Luật Tam đồ thị (TGG) ──────────> Đồ thị Phụ thuộc Luật ───────> Chuỗi Luật & Mô tả Ca kiểm thử (TCD)
                                                                                                      │
                                                                                                      ▼
[Mô hình Kiểm thử Đầu vào] ──> [Động cơ Chuyển đổi (ATL/RTL/QVTr)] ──> [Mô hình Đầu ra] ──> [Hàm Phán xét Bộ phận OCL (USE)] ──> [Báo cáo Lỗi]

Quy trình nghiên cứu rigorous

Quy trình 8 tác vụ kiểm thử tự động khép kín bao gồm:

  1. Đặc tả hệ thống: Thiết kế cam kết chuyển đổi trên giao diện mô hình hóa TC4MT (kết hợp sơ đồ lớp UML và bộ ràng buộc OCL).
  2. Dẫn xuất cài đặt và HOT: Biên dịch đặc tả TC4MT sang các chương trình cài đặt mức thấp (RTL, QVTr, ATL) hoặc làm mịn quy tắc chuyển.
  3. Phân tích phân vùng kết hợp: Phân rã siêu mô hình thành các phân vùng đại diện bản số liên kết ($0, 1, 0.., 1..$), kiểu thuộc tính, kết hợp với các mẫu tiền điều kiện phủ định và bất biến.
  4. Phân tích phụ thuộc luật chuyển đổi: Xây dựng ma trận quan hệ phụ thuộc giữa các luật chuyển đổi tiến ($tr_{F1} \xrightarrow{dep} tr_{F2}$), xác định các điều kiện tiền dung hợp và hậu dung hợp để thiết lập các chuỗi áp dụng luật hợp lệ.
  5. Sinh mô hình kiểm thử tự động: Sử dụng các bộ giải ràng buộc logic chuyên dụng (Kodkod, Alloy Analyzer, UMLtoCSP) để chuyển đổi các biểu thức OCL logic thành các mô hình kiểm thử cụ thể (XMI/USE instance format).
  6. Cấu trúc hàm phán xét bộ phận: Tự động biên dịch các mẫu đồ thị đích trong bất biến và các mô tả ca kiểm thử (TCD) thành các phát biểu xác nhận (OCL assertions).
  7. Thực thi chuyển đổi: Đưa tập mô hình kiểm thử vào động cơ chuyển đổi để sinh các mô hình đích thực tế.
  8. Thẩm định tự động: Đánh giá mô hình đích bằng bộ thẩm định mô hình USE Model Validator, tự động xuất báo cáo vi phạm thuộc tính chất lượng.

Data và phân tích

Quá trình thực nghiệm được triển khai đồng bộ trên trường ca kiểm thử chuyển đổi chuẩn hóa quốc tế CD2RDBM (Class Diagram to Relational Database Model), bao gồm:

  • Tập ca kiểm thử: Hàng chục mô hình kiểm thử cấu trúc phức tạp sinh ra từ các tổ hợp phân vùng khẳng định (Positive Test Suite) và phủ định (Negative Test Suite), kết hợp 100% các đường phụ thuộc luật chuyển.
  • Kỹ thuật phân tích đột biến (Semantic Mutation Analysis): Đánh giá năng lực phát hiện lỗi của bộ ca kiểm thử thông qua việc cấy các đột biến ngữ nghĩa nhân tạo vào chương trình chuyển đổi. Các toán tử đột biến bao gồm:
    • RSCC (Relation Source/Target Class Change): Thay đổi điều hướng quan hệ lớp.
    • ARCR (Attribute Relational Column Replacement): Thay thế sai lệch ánh xạ thuộc tính sang cột.
    • ROCR (Rule Ordering & Condition Removal): Loại bỏ điều kiện áp dụng hoặc đảo lộn thứ tự kích hoạt luật.
  • Độ tin cậy và công cụ: Sử dụng môi trường USE (UML-based Specification Environment), EMF (Eclipse Modeling Framework), bộ giải Kodkod và công cụ Test Bench tự xây dựng của tác giả để tính toán điểm đột biến (Mutation Score - $MS = \frac{M_{killed}}{M_{total}} \times 100%$).

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

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

  1. Vượt qua bài toán NP-Complete trong so khớp mô hình bằng Phán xét bộ phận OCL: Luận án chứng minh thực nghiệm rằng việc sử dụng các xác nhận OCL dẫn xuất từ bất biến TC4MT cho phép phán xét chính xác tính đúng đắn ngữ pháp và bảo toàn thông tin với độ phức tạp thời gian tuyến tính $O(n)$ đối với quy mô phần tử mô hình, giải quyết triệt để bế tắc tính toán của thuật toán đẳng cấu đồ thị ($NP\text{-Complete}$).
  2. Hiệu năng phát hiện lỗi vượt trội của chiến lược kiểm thử phân vùng kết hợp: Bộ ca kiểm thử sinh từ phân tích phân vùng siêu mô hình kết hợp cam kết hành vi đạt điểm đột biến ($MS$) trên 90% đối với các lỗi sai lệch cấu trúc liên kết và vi phạm ràng buộc toàn vẹn khóa chính/khóa ngoại trong ca chuyển đổi CD2RDBM.
  3. Kiểm chứng thành công các thuộc tính chất lượng động (Confluence & Termination): Bằng cách phân tích ma trận phụ thuộc luật TGG, phương pháp kiểm thử của luận án đã phát hiện các xung đột áp dụng luật tiềm ẩn gây bất định (non-confluence) và chu trình lặp vô hạn (non-termination) – những thuộc tính vốn trước đây chỉ có thể tiếp cận bằng chứng minh định lý toán học phức tạp.
  4. Tính hiệu quả của Kiểm thử phủ định (Negative Testing): Việc đưa các mô hình kiểm thử vi phạm tiền điều kiện (ví dụ: lớp tự kế thừa, trùng tên thuộc tính) vào động cơ chuyển đổi cho phép đánh giá chính xác tính vững chắc (robustness) và tính đầy đủ (completeness) của hệ thống chuyển đổi mô hình khi xử lý dữ liệu ngoại lệ.

Implications đa chiều

  • Về mặt Lý thuyết: Cung cấp khung phương pháp luận hoàn chỉnh kết hợp giữa hình thức hóa TGG và kiểm thử hộp đen thực nghiệm, bổ sung một nhánh tri thức quan trọng cho lý thuyết công nghệ phần mềm hướng mô hình.
  • Về mặt Phương pháp luận: Quy trình sinh dữ liệu kiểm thử dựa trên giải ràng buộc OCL từ đặc tả TC4MT có thể chuyển giao và áp dụng trực tiếp cho các hệ thống phần mềm phức tạp khác hoạt động dựa trên cấu trúc đồ thị (như hệ thống xử lý ngôn ngữ miền chuyên biệt DSL, hệ thống tối ưu hóa mã nguồn trình biên dịch).
  • Về mặt Thực tiễn công nghiệp: Giúp các doanh nghiệp phát triển phần mềm quy mô lớn tự động hóa khâu bảo đảm chất lượng trong các pipeline kỹ nghệ MDE, cắt giảm đến 70% thời gian và chi phí thiết kế ca kiểm thử thủ công.
  • Về mặt Chính sách và Tiêu chuẩn hóa: Cung cấp cơ sở khoa học để các tổ chức tiêu chuẩn như OMG mở rộng chuẩn QVT Testing Framework, đưa các tiêu chí kiểm thử cam kết vào tiêu chuẩn phát triển phần mềm hướng kiến trúc MDA.

Limitations và Future Research

Luận án nhìn nhận khách quan 3 giới hạn nghiên cứu chính:

  1. Giới hạn về quy mô phân tích phụ thuộc luật: Khi số lượng quy tắc chuyển đổi TGG tăng lên quy mô hàng trăm luật phức tạp, đồ thị phụ thuộc luật có thể đối mặt với sự bùng nổ tổ hợp các chuỗi kịch bản áp dụng, đòi hỏi các thuật toán heuristic để rút gọn chuỗi kiểm thử.
  2. Phạm vi bảo toàn hành vi mô hình động: Nghiên cứu tập trung chủ yếu vào các mô hình cấu trúc tĩnh (như Class Diagram, Database Schema). Việc kiểm thử tính bảo toàn hành vi động trên các mô hình có ngữ nghĩa thực thi thời gian thực (như Statecharts, Petri Nets) mới dừng lại ở mức đề xuất khung lý thuyết.
  3. Mức độ tự động hóa hoàn toàn của công cụ: Mặc dù các khâu phân tích và phán xét đã được tự động hóa, bước cấu hình giá trị miền biên cho một số kiểu dữ liệu thuộc tính đặc thù vẫn cần sự can thiệp từ tri thức của chuyên gia miền (Domain Expert).

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

  • Phát triển các thuật toán tối ưu hóa thông minh (Meta-heuristic/Search-based Software Testing - SBST) để tự động chọn lọc chuỗi luật chuyển đổi tối ưu.
  • Mở rộng ngôn ngữ TC4MT nhằm đặc tả và kiểm thử tính bảo toàn hành vi động cho các hệ thống hướng sự kiện và hệ thống nhúng an toàn cao.
  • Xây dựng bộ công cụ chuyển đổi mức cao (HOT) hoàn chỉnh, tự động sinh mã kiểm thử song song cho nhiều nền tảng thực thi (ATL, QVTr, Henshin, VIATRA).

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

Nghiên cứu của tác giả Nguyễn Thị Hạnh định hình tầm ảnh hưởng sâu rộng trên nhiều bình diện:

  • Tác động Học thuật: Tạo lập một khung tham chiếu chuẩn mực cho các nghiên cứu tiếp theo về kiểm thử MDE, ước tính đóng góp trích dẫn quan trọng cho các công bố quốc tế thuộc hệ thống ISI/Scopus trong chuyên ngành Software Engineering và Formal Methods.
  • Chuyển đổi Công nghiệp: Ứng dụng trực tiếp vào các ngành công nghiệp đòi hỏi phần mềm độ tin cậy cao như kỹ nghệ ô tô tự hành (Automotive Software qua chuẩn AUTOSAR), hệ thống điều khiển hàng không vũ trụ và các nền tảng chuyển đổi số tài chính ngân hàng vốn phụ thuộc mật thiết vào kiến trúc MDE/MDA.
  • Lợi ích Xã hội: Giảm thiểu rủi ro lỗi phần mềm nghiêm trọng trong các hệ thống hạ tầng trọng yếu, nâng cao năng suất và chất lượng sản phẩm phần mềm quốc gia.

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

  • Nghiên cứu sinh và Giới học thuật: Tiếp cận một khung phương pháp luận kết hợp mẫu mực giữa phương pháp hình thức (TGG) và kiểm thử thực nghiệm, mở ra các đề tài nghiên cứu chuyên sâu về kiểm thử đột biến và giải ràng buộc mô hình.
  • Kỹ sư R&D và Kiến trúc sư phần mềm MDE: Sở hữu công cụ đặc tả trực quan TC4MT và quy trình kiểm thử tự động, giúp thẩm định sớm các đặc tả chuyển đổi trước khi triển khai mã nguồn chi tiết.
  • Chuyên gia Đảm bảo Chất lượng (QA/Test Engineers): Tiếp nhận phương pháp thiết kế bộ ca kiểm thử hộp đen độc lập với ngôn ngữ cài đặt, nâng cao độ bao phủ kiểm thử và năng lực phát hiện khiếm khuyết phần mềm.
  • Các tổ chức chuẩn hóa công nghệ: Có cơ sở dữ liệu thực nghiệm để nâng chuẩn các bộ quy chuẩn kiểm thử mô hình phần mềm quốc tế.

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 hợp nhất mô hình phân tầng cam kết 4 cấp độ vào hệ thống Văn phạm tam đồ thị (TGG) của Schürr (1994), mở rộng nguyên lý Thiết kế theo cam kết của Meyer (1992) sang miền chuyển đổi mô hình. Luận án đã giải quyết bài toán biểu diễn đồng thời cấu trúc dữ liệu tĩnh và bước chuyển động bằng một cú pháp hình thức thống nhất.

2. Điểm đột phá về phương pháp luận của luận án so với các nghiên cứu quốc tế trước đây là gì?
So với nghiên cứu của Fleurey et al. (2009) vốn chỉ phân vùng dựa trên siêu mô hình nguồn và nghiên cứu của Barroca et al. (2011) với DSLTrans bị giới hạn trong việc kiểm chứng thuộc tính, luận án tích hợp ma trận phụ thuộc luật TGG với kỹ thuật giải ràng buộc OCL (thông qua Kodkod/Alloy). Điều này cho phép sinh tự động cả mô hình kiểm thử lẫn hàm phán xét bộ phận, kiểm chứng được đồng thời 5 thuộc tính chất lượng chức năng (ngữ pháp, bảo toàn thông tin, bảo toàn hành vi, hội tụ, kết thúc) mà không phụ thuộc vào ngôn ngữ cài đặt.

3. Phát hiện thực nghiệm bất ngờ nhất được hỗ trợ bởi dữ liệu trong luận án là gì?
Phát hiện chỉ ra rằng việc kiểm thử khẳng định thuần túy chỉ phát hiện được các lỗi ánh xạ bề mặt, trong khi kiểm thử phủ định dựa trên tiền điều kiện kết hợp với đột biến điều hướng quan hệ (RSCC) giúp nâng điểm đột biến ($MS$) phát hiện các lỗi ngữ nghĩa tiềm ẩn trong các bộ chuyển đổi phức tạp từ mức trung bình 60% lên trên 90%.

4. Luận án có cung cấp quy trình tái lập (Replication Protocol) hoàn chỉnh không?
Hoàn toàn có. Luận án mô tả chi tiết kiến trúc công cụ TC4MT Test Bench tích hợp trên môi trường USE, công thức hóa các thuật toán sinh chuỗi luật, cung cấp đầy đủ tập luật tam đồ thị mẫu của ca chuyển đổi CD2RDBM và các toán tử đột biến ngữ nghĩa, tạo điều kiện thuận lợi cho việc tái lập và kiểm chứng độc lập.

5. Chương trình nghị sự nghiên cứu 10 năm (10-year research agenda) được định hình như thế nào?
Lộ trình 10 năm mở rộng từ: (1) Hoàn thiện bộ công cụ HOT tự động cho các ngôn ngữ MDE công nghiệp; (2) Ứng dụng Trí tuệ nhân tạo (AI/Search-based testing) trong tối ưu hóa không gian mô hình kiểm thử; đến (3) Mở rộng khung hình thức TC4MT sang kiểm thử các hệ thống chuyển đổi mô hình tự thích nghi (Self-adaptive Systems) và hệ thống Cyber-Physical Systems (CPS) phức hợp.

Kết luận

Luận án tiến sĩ của tác giả Nguyễn Thị Hạnh là một công trình khoa học xuất sắc, mẫu mực về tính hình thức toán học và giá trị ứng dụng thực tiễn trong chuyên ngành Kỹ thuật phần mềm. 5 đóng góp đột phá cốt lõi bao gồm:

  1. Xây dựng thành công ngôn ngữ đặc tả chuyển đổi mô hình dựa trên cam kết TC4MT, sở hữu ngữ nghĩa hình thức dựa trên Văn phạm tam đồ thị (TGG) và cú pháp trực quan kết hợp UML/OCL.
  2. Đề xuất phương pháp phân tích phân vùng kết hợp siêu mô hình và cam kết hành vi, thiết lập chiến lược sinh tập ca kiểm thử khẳng định và phủ định toàn diện.
  3. Tiên phong phát triển kỹ thuật phân tích quan hệ phụ thuộc giữa các quy tắc chuyển đổi TGG để thiết kế mô tả ca kiểm thử (TCD) theo hướng tiếp cận kiểm thử văn phạm.
  4. Cấu trúc hóa hoàn chỉnh hệ thống các hàm phán xét kiểm thử bộ phận bằng các xác nhận OCL, giải quyết triệt để bài toán khó $NP\text{-Complete}$ của so khớp đồ thị đầu ra.
  5. Hiện thực hóa khung công cụ thực nghiệm trên môi trường USE, kiểm chứng định lượng năng lực phát hiện lỗi thông qua phân tích đột biến ngữ nghĩa trên các bài toán chuyển đổi mô hình tiêu chuẩn.

Công trình tạo ra bước tiến quan trọng trong việc đảm bảo độ tin cậy của các hệ thống phát triển dựa trên mô hình, mở ra các hướng nghiên cứu mới về kiểm thử phần mềm tự động hóa và khẳng định năng lực học thuật đỉnh cao của nghiên cứu sinh trong cộng đồng Kỹ nghệ phần mềm quốc tế.