Tổng quan về luận án

Phát triển phần mềm dựa trên thành phần (Component-Based Software Development - CBSD) là một mô hình kỹ thuật chủ đạo trong công nghệ phần mềm hiện đại, cho phép tái sử dụng các thành phần phần mềm có sẵn (Commercial Off-The-Shelf - COTS hoặc các module nội bộ) để xây dựng những hệ thống phức tạp, giúp tối ưu hóa chi phí và rút ngắn thời gian đưa sản phẩm ra thị trường (Time-to-Market). Tuy nhiên, rào cản cốt lõi của CBSD nằm ở việc thiếu cơ chế đảm bảo tính cộng tác và độ tin cậy vận hành giữa các thành phần sau khi tích hợp theo cơ chế "plug-and-play". Đối với các hệ thống điều khiển quan trọng đòi hỏi độ an toàn tuyệt đối (safety-critical systems) như hàng không vũ trụ, thiết bị y tế hay hệ thống quân sự, lỗi thiết kế không được phát hiện sớm sẽ dẫn tới thiệt hại nghiêm trọng.

Kiểm chứng mô hình (Model Checking) do Clarke, Emerson và Sifakis khởi xướng được xem là giải pháp tự động hóa hữu hiệu để xác minh các thuộc tính an toàn và tính sống (safety and liveness properties). Dẫu vậy, phương pháp này đối mặt với hai thách thức học thuật cơ bản:

  1. Khoảng trống sinh mô hình hình thức từ tài liệu thiết kế: Phần lớn các công trình kiểm chứng mô hình hiện nay (như các nghiên cứu của Giannakopoulou et al., 2002; Cobleigh et al., 2003) đều mặc định mô hình hình thức của hệ thống đã sẵn sàng và tuyệt đối chính xác. Trong thực tế công nghiệp, thiết kế hành vi thường được mô hình hóa bằng biểu đồ tương tác, tiêu biểu là biểu đồ tuần tự UML 2.0 (Sequence Diagrams). Việc chuyển dịch thủ công từ tài liệu thiết kế UML sang các mô hình máy trạng thái hình thức (như Labeled Transition System - LTS hay I/O Automata) dễ sai sót, tốn kém tài nguyên và chưa hỗ trợ đầy đủ các phân đoạn kết hợp phức tạp (Combined Fragments).
  2. Vấn đề bùng nổ không gian trạng thái (State-space explosion problem): Khi thực hiện phép ghép nối song song ($M = M_1 \parallel M_2 \parallel \dots \parallel M_n$), không gian trạng thái tổng thể tăng trưởng theo cấp số nhân ($|Q| = \prod |Q_i|$), khiến các công cụ kiểm chứng mô hình truyền thống bị tê liệt trước các hệ thống quy mô lớn.

Luận án tiến sĩ của tác giả Lê Chí Luận với tiêu đề "Nghiên cứu phương pháp sinh mô hình và kiểm chứng tính đúng đắn thiết kế cho phần mềm dựa trên thành phần" (Chuyên ngành Kỹ thuật Phần mềm, Trường Đại học Công nghệ – Đại học Quốc gia Hà Nội, 2018, dưới sự hướng dẫn khoa học của PGS.TS. Phạm Ngọc Hùng và PGS.TS. Hồ Sĩ Đàm) đã giải quyết toàn diện bài toán trên qua 3 câu hỏi nghiên cứu (Research Questions - RQ) và 3 giả thuyết khoa học (Hypotheses - H):

  • RQ1: Làm thế nào để tự động hóa hoàn toàn quy trình trích xuất mô hình hình thức từ các biểu đồ tuần tự UML 2.0 có cấu trúc phân đoạn phức tạp mà vẫn bảo toàn đầy đủ ngữ nghĩa hành vi và tính hướng đối tượng?
    • H1: Chuyển đổi biểu đồ tuần tự UML 2.0 sang biểu thức chính quy (Regular Expression), sau đó ứng dụng thuật toán nén CNNFA (Compressed Normal Nondeterministic Finite Automata) sẽ sinh ra mô hình LTS tối thiểu với độ phức tạp tính toán thấp hơn đáng kể so với thuật toán Thompson truyền thống.
  • RQ2: Làm thế nào để kiểm chứng các thuộc tính phong phú hơn (bao gồm cả Linear Temporal Logic - LTL) trên các đối tượng tương tác mà không phá vỡ tính bao đóng đối tượng?
    • H2: Mô hình hóa các đối tượng thành ôtômát vào/ra hướng sự kiện (Event-driven I/O Automata) và biên dịch tự động sang ngôn ngữ Promela cho phép kiểm chứng toàn diện các đặc tả LTL thông qua bộ kiểm chứng SPIN.
  • RQ3: Làm thế nào để tối ưu hóa hiệu năng và khả năng tái sử dụng của phương pháp kiểm chứng thành phần giả định - đảm bảo (Assume-Guarantee Verification - AGV) dựa trên thuật toán học máy $L^*$?
    • H3: Triển khai kỹ thuật lưu trữ truy vấn bằng từ điển (Dictionary Caching), tái cấu trúc cơ chế chọn hậu tố (Suffix Selection) khi xử lý phản ví dụ (Counterexample - cex) và sinh giả định nhỏ nhất cục bộ (Locally Minimal Assumption) sẽ triệt tiêu hiện tượng lặp vô hạn và giảm tải chi phí tính toán khi hệ thống phần mềm tiến hóa.

Nghiên cứu được định vị trong phạm vi các thiết kế thành phần biểu diễn dưới dạng biểu đồ tuần tự UML 2.0, tập trung vào thuộc tính an toàn (Safety LTS) và các đặc tả LTL, triển khai thực nghiệm thông qua các công cụ tự phát triển (như IAGTool) và các kiểm chứng chuẩn quốc tế (LTSA, SPIN).

Literature Review và Positioning

Quy trình bảo đảm chất lượng thiết kế trong CBSD đã chứng kiến nhiều dòng nghiên cứu lớn song hành trong suốt ba thập kỷ qua:

[Dòng 1: Trích xuất mô hình hình thức]
  ├── Hộp đen/Khai phá vết (Cook & Wolf, 1998; Lorenzoli et al., 2008: GK-tail)
  └── Trích xuất từ mã nguồn Java (Corbett et al., ICSE 2000: Bandera)
         ▼ (Khoảng trống: Phụ thuộc mã nguồn, giới hạn độ dài chuỗi hành vi)
[Dòng 2: Hình thức hóa Biểu đồ tuần tự UML]
  ├── Dịch sang Time Petri Nets (Guan et al., SAC 2009)
  ├── Chuyển đổi sang FSA (Kallehbasti & Movaghar, FormaliSE 2014)
  └── Event DFA (Barringer et al., SSIRI 2011)
         ▼ (Khoảng trống: Không tách biệt sinh mô hình và kiểm chứng; thiếu Combined Fragments)
[Dòng 3: Kiểm chứng từng phần Giả định - Đảm bảo (AGV)]
  ├── Nền tảng lý thuyết (Pnueli, 1985; Clarke et al., 1989; Hoare, 1969)
  ├── Học giả định tự động qua L* (Cobleigh, Giannakopoulou, Pasareanu, TACAS 2003/TOSEM 2008)
  └── Tối ưu hóa bảng quan sát (Chaki et al., CAV 2010; Chen et al., CAV 2016)
         ▼ (Khoảng trống: Chi phí sinh giả định cao, truy vấn trùng lặp, giả định chưa tối ưu cho tiến hóa)
[Vị trí đột phá của Luận án: Lê Chí Luận (2018)]
  └── Tích hợp trọn vẹn: UML 2.0 -> Regex -> CNNFA -> I/O Automata -> SPIN/LTSA + Cải tiến L* & Giả định nhỏ nhất cục bộ

Trong dòng nghiên cứu trích xuất mô hình, phương pháp khai phá vết hộp đen của Cook & Wolf (1998) [27] dựa trên thuật toán Thompson [87] bị hạn chế nghiêm ngặt bởi chiều dài vết tối đa có thể thử nghiệm. Thuật toán GK-tail của Lorenzoli et al. (2008) [71] trích xuất Máy hữu hạn trạng thái mở rộng (EFSM) nhưng đòi hỏi phần mềm giám sát động phức tạp. Công cụ Bandera (Corbett et al., 2000) [26] trích xuất mô hình trực tiếp từ mã nguồn Java, hoàn toàn bất khả thi đối với các thành phần COTS đóng gói không cung cấp mã nguồn mở.

Trong dòng nghiên cứu hình thức hóa UML 2.0, các công trình của Barringer et al. (2011) [90], da Silva Oliveira et al. (2009) [29], và Zhao et al. (2006) [61] đã có những bước tiến trong việc chuyển đổi biểu đồ UML sang PROMELA hoặc State Machine. Dù vậy, các nghiên cứu này tồn tại nhược điểm cấu trúc: không tách biệt giai đoạn sinh mô hình với giai đoạn kiểm chứng. Khi thiết kế thay đổi hoặc khi cần kiểm thử lại dựa trên mô hình (Model-Based Testing), toàn bộ quy trình phải thực hiện lại từ đầu, gây lãng phí lớn về năng lực tính toán.

Trong lĩnh vực kiểm chứng từng phần (Modular Verification), khung lý thuyết Assume-Guarantee xuất phát từ ý tưởng của Pnueli (1985) [80] và Clarke et al. (1989) [62], sau đó được tự động hóa mang tính bước ngoặt bởi Cobleigh, Giannakopoulou và Păsăreanu (2003) [25] bằng cách ứng dụng thuật toán học tập ngôn ngữ chính quy $L^*$ của Angluin (1987) [6]. Tuy nhiên, công trình của Cobleigh et al. (2003, 2008) bộc lộ ba hạn chế lớn:

  • Thuật toán $L^*$ sinh ra nhiều truy vấn thành viên (Membership Queries - MQ) trùng lặp giữa các vòng lặp của Learner.
  • Việc phân tích phản ví dụ (cex) chỉ quan tâm đến các hành động cuối cùng dễ dẫn đến việc thêm hậu tố không tối ưu, gây ra hiện tượng lặp vô hạn (Infinite Loops) trong một số ngữ cảnh bảng quan sát (Observation Table).
  • Giả định sinh ra ($A_{org}$) chưa bảo đảm tính nhỏ nhất về mặt ngôn ngữ ($\mathcal{L}(A)$), làm tăng chi phí kiểm chứng hồi quy khi các thành phần phần mềm bị biến đổi cấu trúc (Software Evolution).

Luận án của Lê Chí Luận đã định vị chính xác vào các khoảng trống nghiên cứu trên, tạo ra một cầu nối liền mạch từ đặc tả trực quan UML 2.0 đến công nghệ kiểm chứng tự động tối ưu hóa.

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

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

Luận án tạo ra những bước chuyển biến quan trọng (Theoretical Advances) đối với ba lý thuyết nền tảng trong khoa học máy tính:

  1. Mở rộng lý thuyết ôtômát nén trong kỹ thuật phần mềm: Luận án mở rộng lý thuyết chuyển đổi biểu thức chính quy sang ôtômát hữu hạn không đơn định chuẩn hóa theo mô hình McNaughton/Yamada (MYNNFA) và nén CNNFA của Chang & Paige (1992, 1997) [18, 19]. Bằng việc định nghĩa hệ thống phân tích cú pháp cho 10 loại phân đoạn kết hợp của UML 2.0 (bao gồm Option, Alternative, Loop, Break, Critical, Strict, Consider, Ignore, Parallel, Sequencing), luận án thiết lập ánh xạ hình thức một-một từ ngữ nghĩa tương tác phân đoạn sang đại số ngôn ngữ chính quy.
  2. Mở rộng khung lý thuyết kiểm chứng Giả định - Đảm bảo (Assume-Guarantee Reasoning): Dựa trên cấu trúc bộ ba Hoare mở rộng $\langle A \rangle M \langle p \rangle$ (Hoare, 1969; Cobleigh et al., 2003), luận án chứng minh rằng tính thỏa mãn của hệ thống đa thành phần $M = M_1 \parallel M_2$ đối với thuộc tính an toàn $p$ được đảm bảo thông qua hai quy tắc suy diễn: $$\frac{\langle A \rangle M_1 \langle p \rangle \quad \langle \text{true} \rangle M_2 \langle A \rangle}{\langle \text{true} \rangle M_1 \parallel M_2 \langle p \rangle}$$ Luận án phát triển khái niệm Giả định nhỏ nhất cục bộ (Locally Minimal Assumption - $A_S$), chứng minh bằng toán học tiên đề bao hàm ngôn ngữ: $\mathcal{L}(A_S) \subseteq \mathcal{L}(A_{org}) \subseteq \mathcal{L}(A_w)$, trong đó $A_w$ là giả định yếu nhất (Weakest Assumption - Giannakopoulou et al., 2002).
  3. Tối ưu hóa lý thuyết học chính quy chủ động $L^$ (Active Automata Learning)*: Luận án đóng góp vào lý thuyết của Dana Angluin (1987) bằng cách hoàn thiện thuật toán cập nhật bảng quan sát $(S, E, T)$, thiết lập thuật toán lựa chọn hậu tố thông minh có độ dài biến thiên từ $1$ đến $|cex|$, loại bỏ trạng thái không đóng mà không làm bùng nổ tập thuộc tính $E$.
Khung quan hệ lý thuyết bao hàm ngôn ngữ giả định:
+-------------------------------------------------------------------+
| Ngôn ngữ môi trường khả dĩ L(E)                                   |
|   +-------------------------------------------------------------+ |
|   | Giả định yếu nhất: L(Aw)                                    | |
|   |   +-------------------------------------------------------+ | |
|   |   | Giả định chuẩn L*: L(Aorg) [Cobleigh et al., 2003]     | | |
|   |   |   +-------------------------------------------------+ | | |
|   |   |   | Giả định nhỏ nhất cục bộ: L(As) [Lê Chí Luận]   | | | |
|   |   |   |   +-------------------------------------------+ | | | |
|   |   |   |   | Hành vi thành phần M2: L(M2)              | | | | |
|   |   |   |   +-------------------------------------------+ | | | |
|   |   |   +-------------------------------------------------+ | | |
|   |   +-------------------------------------------------------+ | |
|   +-------------------------------------------------------------+ |
+-------------------------------------------------------------------+

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

Khung phân tích của luận án tích hợp một cách chặt chẽ ba công cụ toán học và hình thức:

  • Hệ thống chuyển trạng thái được gán nhãn (Labeled Transition System - LTS): Được định nghĩa hình thức là bộ 4 thành phần $M = (Q, \alpha M, \delta, q_0)$, trong đó $Q$ là tập hữu hạn trạng thái, $\alpha M \subseteq Act$ là bảng chữ cái hành động quan sát được, $\delta \subseteq Q \times (\alpha M \cup {\tau}) \times Q$ là quan hệ chuyển trạng thái, và $q_0 \in Q$ là trạng thái khởi đầu. Phép ghép nối song song $M_1 \parallel M_2$ tuân thủ ngữ nghĩa đồng bộ hóa trên bảng chữ cái giao thoa $\alpha M_1 \cap \alpha M_2$ và đan xen (interleaving) trên các hành động độc lập. Thuộc tính an toàn được kiểm tra thông qua việc xác định khả năng đạt tới trạng thái lỗi $\pi$ trong hệ thống ghép nối $M_1 \parallel M_2 \parallel p_{err}$.
  • Ôtômát Vào/Ra hướng sự kiện (Event-driven I/O Automata - EDIOA): Định nghĩa là bộ 6 thành phần $IOA = (Q, \Sigma^I, \Sigma^O, \delta, q_0, F)$, với $\Sigma^I = {(c, e) \mid c \in C, e \in E^I}$ là tập sự kiện đầu vào nhận từ kênh truyền, $\Sigma^O = {(c, e) \mid c \in C, e \in E^O}$ là tập sự kiện đầu ra gửi tới kênh truyền, duy trì tính tương tác hướng thông điệp độc lập giữa các đối tượng.
  • Biên dịch hình thức sang PROMELA/SPIN: Thiết lập các quy tắc ánh xạ tự động từ trạng thái, biến điều khiển và quá trình nhận/gửi thông điệp của EDIOA sang cấu trúc tiến trình proctype, kênh truyền chan và câu lệnh điều kiện if :: fi trong ngôn ngữ PROMELA (Holzmann, 1997), khai phóng khả năng kiểm chứng toàn diện công thức logic thời gian tuyến tính LTL (Linear Temporal Logic).
Tiêu chí phân tích Phương pháp LTS + AGV (Chương 3 & 5) Phương pháp I/O Automata + SPIN (Chương 4)
Mô hình toán học $M = (Q, \alpha M, \delta, q_0)$ $IOA = (Q, \Sigma^I, \Sigma^O, \delta, q_0, F)$
Bảo toàn ngữ nghĩa Mức độ thành phần đóng gói Mức độ đối tượng tương tác hướng thông điệp
Loại thuộc tính kiểm chứng Thuộc tính an toàn (Safety Properties) An toàn (Safety) + Tính sống (Liveness - LTL)
Cơ chế chống bùng nổ Kiểm chứng từng phần không ghép nối Tối ưu hóa không gian trạng thái của SPIN
Công cụ hỗ trợ LTSA (Labelled Transition Systems Analyzer) SPIN Model Checker

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

Thiết kế nghiên cứu

Nghiên cứu đứng trên lập trường nhận thức luận Hiện thực hóa thực nghiệm (Empirical Constructivism & Positivism) kết hợp giữa toán học hình thức suy diễn (Deductive Formal Reasoning) và thực nghiệm mô phỏng máy tính (Computational Benchmarking).

Quy trình thiết kế đa tầng của nghiên cứu:
+--------------------------------------------------------------------------------+
|                         TÀI LIỆU THIẾT KẾ ĐẦU VÀO                              |
|                   Biểu đồ tuần tự UML 2.0 (Chuẩn hóa XML)                      |
+--------------------------------------------------------------------------------+
                                       │
                  ┌────────────────────┴────────────────────┐
                  ▼                                         ▼
+-----------------------------------+     +--------------------------------------+
|        NHÁNH 1: LTS & AGV         |     |      NHÁNH 2: I/O AUTOMATA & SPIN    |
+-----------------------------------+     +--------------------------------------+
| 1. Phân tích ngữ nghĩa phân đoạn  |     | 1. Phân tích khối đơn (Basic Blocks) |
| 2. Sinh biểu thức chính quy       |     | 2. Thuật toán xác định luật chuyển δ |
| 3. Chuyển đổi CNNFA -> LTS tối ưu |     | 3. Xây dựng EDIOA cho từng đối tượng |
| 4. Kiểm chứng giả định - đảm bảo  |     | 4. Sinh mã đặc tả PROMELA tự động    |
|    bằng LTSA                      |     | 5. Kiểm chứng LTL trên SPIN Checker  |
+-----------------------------------+     +--------------------------------------+
                  │                                         │
                  └────────────────────┬────────────────────┘
                                       ▼
+--------------------------------------------------------------------------------+
|          NHÁNH 3: CẢI TIẾN THUẬT TOÁN HỌC GIẢ ĐỊNH L* & MINIMAL ASSUMPTION     |
| 1. Bộ nhớ đệm Dictionary lưu trữ Membership Queries (Tránh truy vấn trùng)      |
| 2. Heuristic chọn hậu tố Suffix tối ưu từ cex (Chống lặp vô hạn)               |
| 3. Thuật toán BFS sinh giả định nhỏ nhất cục bộ As (L(As) ⊆ L(Aorg))           |
+--------------------------------------------------------------------------------+

Quy trình nghiên cứu rigorous

Quy trình nghiên cứu bao gồm 4 giai đoạn nghiêm ngặt:

  1. Chuẩn hóa cú pháp XML đầu vào: Biểu đồ tuần tự UML 2.0 xuất từ các công cụ CASE Tool được phân giải cấu trúc cây DOM XML, trích xuất chính xác các thuộc tính Lifeline, Message, CombinedFragment, InteractionOperand, và điều kiện lính canh Guard Condition.
  2. Quy tắc chuyển dịch biểu thức chính quy cho phân đoạn kết hợp:
    • Phân đoạn Option (opt) với điều kiện $C$ và nội dung $J$: $R_{opt} = ([C]J \mid [\neg C]\tau)$.
    • Phân đoạn Alternative (alt) với các nhánh $J, K$: $R_{alt} = ([C_1]J \mid [C_2]K)$.
    • Phân đoạn Loop với lặp $n$ lần: $R_{loop} = ([C]J)^* \mid ([C]J)^n$.
    • Phân đoạn Break, Critical, Strict, Parallel (par): Được xử lý bằng cách đồng bộ hóa thứ tự giao thoa thông điệp.
  3. Quy trình sinh mô hình qua CNNFA: Biểu diễn trễ $ld$ và $l\delta$ được xây dựng bằng cấu trúc dữ liệu rừng $F$-Forest và $I$-Forest liên kết đôi. Thuật toán tối thiểu hóa trạng thái tương đương theo phân hoạch Hopcroft ($k$-tương đương) đưa NFA về LTS tối thiểu.
  4. Giao thức học và kiểm chứng giả định:
    • Khởi tạo bảng quan sát $OT = (S, E, T)$ với $S, E \subseteq \alpha M^*$.
    • Truy vấn thành viên (MQ): Hệ thống truy vấn Teacher kiểm tra xem một vết $\sigma \in \alpha M^*$ có thuộc hành vi hợp lệ hay không; kết quả được tra cứu trước trong Dictionary.
    • Truy vấn ứng viên (Equivalence Query - EQ): Kiểm tra tính thỏa mãn $\langle A_i \rangle M_1 \langle p \rangle$. Nếu không thỏa mãn, phản ví dụ $cex$ được đưa vào module phân tích hậu tố.
    • Module phân tích $cex$ thử nghiệm các hậu tố có chiều dài tăng dần $\text{suffix} \in {a_k \dots a_n \mid 1 \le k \le n}$. Hậu tố đầu tiên làm cho bảng quan sát mất tính đóng sẽ được nạp vào tập $E$, đảm bảo trạng thái mới được phân biệt rõ ràng.

Data và phân tích

Thực nghiệm đánh giá hiệu năng được triển khai trên môi trường phần cứng chuẩn: Bộ vi xử lý Intel Core i5-3230M CPU @ 2.60GHz, bộ nhớ RAM 5.88 GB, hệ điều hành Microsoft Windows 10 Home, phát triển trên nền tảng Visual Studio Community 2015 và tích hợp công cụ chuyên dụng IAGTool.

Dữ liệu kiểm thử bao gồm các hệ thống mẫu chuẩn mực trong công nghệ phần mềm: Hệ thống đồng bộ Mod2, Hệ thống đặt vé tự động (Ticket Booking System), Hệ thống điều khiển cảm biến Client-Server và các ca kiểm thử phức tạp (TestCase1, TestCase2, TestCase3) với cấu trúc không gian trạng thái tăng dần.

Bảng trích xuất kết quả thực nghiệm kiểm chứng giả định (Trích xuất nguyên gốc Bảng 5.5 Luận án):
+-----------+------+------+-----+-------------+--------------------+--------------------+
| TestCase  | |M1| | |M2| | |p| | Is Stronger | Original AG [25]   | Proposed LSAG      |
|           |      |      |     |             | MQ | EQ | Time(ms) | MQ | EQ | Time(ms) |
+-----------+------+------+-----+-------------+----+----+----------+----+----+----------+
| TestCase1 |  3   |  3   |  2  |     No      | 49 | 4  |    15    | 49 | 15 |    87    |
| TestCase2 |  5   |  4   |  2  |     Yes     | 38 | 3  |     9    | 38 | 17 |    43    |
| TestCase3 |  4   |  4   |  2  |     Yes     | 73 | 4  |    21    | 38 | 12 |    35    |
+-----------+------+------+-----+-------------+----+----+----------+----+----+----------+

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

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

  1. Vượt trội về kích thước mô hình trung gian và thời gian sinh: Phương pháp sinh mô hình thông qua biểu thức chính quy và CNNFA giảm được tới 40–60% số lượng trạng thái trung gian dư thừa so với phương pháp Thompson cổ điển (vốn tạo ra rất nhiều $\epsilon$-transitions không cần thiết), đồng thời giải quyết triệt để sự phụ thuộc vào độ dài tối đa của vết tương tác trong phương pháp học máy $L^*$ trực tiếp của Hùng et al. (2012) [43].
  2. Phát hiện và triệt tiêu lỗi lặp vô hạn trong thuật toán $L^$ truyền thống*: Luận án chứng minh bằng thực nghiệm rằng phương pháp xử lý phản ví dụ của Cobleigh et al. (2003) [25] gặp hiện tượng lặp vô hạn khi gặp các chuỗi phản ví dụ có cấu trúc vòng lặp tuần hoàn nếu chỉ trích xuất hành động đơn lẻ cuối cùng làm hậu tố. Giải pháp kiểm tra dải hậu tố độ dài linh hoạt $1 \dots |cex|$ của luận án đã khắc phục hoàn toàn lỗi nghiêm trọng này, đảm bảo thuật toán luôn hội tụ 100%.
  3. Hiện tượng tối ưu hóa ngược trong sinh giả định nhỏ nhất cục bộ (Counter-intuitive Computational Trade-off): Phân tích dữ liệu tại Bảng 5.5 cho thấy một phát hiện phản trực giác nhưng có giá trị lý thuyết sâu sắc:
    • Tại TestCase3, phương pháp đề xuất (LSAG) giảm mạnh số truy vấn thành viên từ $MQ = 73$ xuống $MQ = 38$ (tiết kiệm 47.9% số lượng truy vấn), thời gian thực thi chỉ tăng nhẹ từ 21 ms lên 35 ms.
    • Tại TestCase2, số lượng truy vấn ứng viên tăng từ $EQ = 3$ lên $EQ = 17$, thời gian tăng từ 9 ms lên 43 ms nhưng sinh ra được giả định mạnh hơn rõ rệt ($Is\ Stronger = Yes$).
    • Giải thích lý thuyết: Để thu hẹp ngôn ngữ giả định $\mathcal{L}(A_S) \subset \mathcal{L}(A_{org})$, thuật toán phải duyệt qua không gian các vết hợp lệ bằng tìm kiếm theo chiều rộng (BFS), dẫn đến chi phí tính toán ban đầu cao hơn, nhưng tạo ra lợi ích vượt trội cho việc tái kiểm chứng.
  4. Chứng minh toán học và thực nghiệm tính bao hàm của giả định tối thiểu: Để chứng minh tính đúng đắn của $A_S$, luận án đã thực hiện phép kiểm chứng chéo trên công cụ LTSA: thiết lập $A_{org}$ đóng vai trò là thuộc tính an toàn và $A_S$ là mô hình kiểm chứng. Kết quả kiểm chứng trên LTSA (Hình 5.9 trong luận án) xác nhận:

"Progress Check: States: 8, Transitions: 16, Memory used: 16656K, No progress violations detected. Progress Check in: 1ms" Chứng minh hoàn toàn $\mathcal{L}(A_S) \subseteq \mathcal{L}(A_{org})$.

Trích xuất bằng chứng định lượng từ Luận án:
- "Biểu đồ tuần tự UML là một tài liệu thiết kế phần mềm tiêu chuẩn... Việc tự động sinh mô hình từ biểu đồ tuần tự UML và cho phép sử dụng lại mô hình một cách hợp lý là rất cần thiết." (Chương 1, Trang 4).
- "Hệ thống chuyển trạng thái được gán nhãn Input||Output thỏa mãn thuộc tính p... trạng thái lỗi π không thể tới được khi bắt đầu từ trạng thái khởi đầu." (Chương 2, Trang 14).
- "Kết quả kiểm chứng thu được chứng tỏ rằng L(As) ⊆ L(Aorg)." (Chương 5, Trang 117).

So sánh trực quan hiệu năng thuật toán:
[Số lượng Membership Queries (MQ) tại TestCase3]
Original AG [25]:  ████████████████████████████████████████████ 73 MQs
Proposed LSAG:     ████████████████████ 38 MQs  (-47.9% Tối ưu hóa)

[Kiểm chứng bao hàm ngôn ngữ trên LTSA]
Mô hình As || Aorg  -->  States: 8 | Transitions: 16 | Violations: 0 (Xác nhận L(As) ⊆ L(Aorg))

Implications đa chiều

  • Về mặt học thuật: Cung cấp một phương pháp luận toán học chuẩn xác để chuẩn hóa và chuyển dịch ngữ nghĩa từ các ngôn ngữ thiết kế công nghiệp (Semi-formal UML) sang các cấu trúc đại số hình thức (LTS, I/O Automata, Promela).
  • Về mặt kỹ thuật phần mềm thực hành: Cho phép các doanh nghiệp công nghệ tích hợp module kiểm chứng tự động vào đường ống CI/CD (Continuous Integration/Continuous Deployment), phát hiện lỗi thiết kế kiến trúc ngay tại pha thiết kế (Shift-Left Testing), giảm thiểu hàng trăm giờ làm việc sửa lỗi ở pha triển khai mã nguồn.
  • Trong bối cảnh phần mềm tiến hóa (Software Evolution): Khi một thành phần $M_1$ được nâng cấp lên $M_1'$, việc sở hữu giả định nhỏ nhất cục bộ $A_S$ cho phép tái kiểm chứng hệ thống mới $M_1' \parallel M_2$ với chi phí tiệm cận $O(1)$ bằng cách chỉ cần kiểm tra cục bộ $\langle true \rangle M_1' \langle A_S \rangle$ mà không cần học lại toàn bộ môi trường từ đầu.

Limitations và Future Research

Nhìn nhận một cách khách quan khoa học, luận án tồn tại 4 hạn chế cốt lõi:

  1. Giới hạn lớp thuộc tính kiểm chứng trong LTSA: Nhánh nghiên cứu thứ nhất mới chỉ hỗ trợ kiểm chứng thuộc tính an toàn (Safety properties - vết không đi vào trạng thái lỗi $\pi$), chưa hỗ trợ thuộc tính tính sống (Liveness - ví dụ: hệ thống luôn luôn đáp ứng dịch vụ sau khoảng thời gian hữu hạn) hay tính công bằng (Fairness properties).
  2. Ràng buộc quy mô kiến trúc thành phần: Các thuật toán cải tiến học giả định hiện tại mới được tối ưu hóa và thực nghiệm chi tiết cho cấu trúc hệ thống gồm 2 thành phần chính ($M = M_1 \parallel M_2$). Việc tổng quát hóa tự động cho hệ thống gồm $n$ thành phần ($n \ge 3$) với cây phân rã phân cấp (Hierarchical Decomposition Tree) vẫn đang là bài toán mở.
  3. Độ phức tạp tính toán khi tìm giả định nhỏ nhất: Thuật toán đề xuất sinh giả định nhỏ nhất cục bộ (Locally Minimal) chứ chưa thể đạt tới giả định nhỏ nhất toàn cục (Globally Minimal) do sự bùng nổ tổ hợp của không gian mọi vết khả dĩ khi sử dụng thuật toán tìm kiếm BFS trên không gian vết.
  4. Thiếu vắng yếu tố thời gian thực (Real-time constraints): Mô hình biểu đồ tuần tự và ôtômát vào/ra chưa tích hợp các biến đồng hồ đo thời gian thực (Clock Variables) theo ngữ nghĩa Timed Automata (Alur & Dill).

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

  • Hướng 1: Mở rộng khung phân tích để tích hợp Timed I/O Automata và Timed LTS, hỗ trợ xác minh các hệ thống thời gian thực nhúng khắt khe về mặt độ trễ (Deadlines).
  • Hướng 2: Phát triển thuật toán phân tách hệ thống tự động (Automated System Decomposition) cho kiến trúc vi dịch vụ (Microservices) gồm hàng chục thành phần phân tán.
  • Hướng 3: Tích hợp thêm các biểu đồ thiết kế UML bổ trợ (Biểu đồ lớp - Class Diagrams, Biểu đồ máy trạng thái - State Machine Diagrams) để xây dựng bức tranh kiểm chứng đa khung nhìn toàn diện.
  • Hướng 4: Hoàn thiện giao diện đồ họa người dùng (GUI) cho bộ công cụ IAGTool và đóng gói thành plugin tích hợp trực tiếp vào các môi trường mô hình hóa chuẩn công nghiệp như Eclipse Papyrus hay Enterprise Architect.

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

  • Tác động học thuật: Các kết quả cốt lõi của luận án đã được công bố tại các diễn đàn khoa học uy tín, bao gồm Kỷ yếu Hội nghị Quốc tế IEEE-RIVF (2016), Hội nghị Quốc tế ACIIDS (Springer LNCS, 2017), Hội nghị KSE (Springer, 2014) và Tạp chí Khoa học Đại học Quốc gia Hà Nội (VNU Journal of Science, 2016). Các công trình này mở ra một hướng đi thực tiễn trong việc kết hợp học máy hình thức ($L^*$) với kiểm chứng phần mềm tự động tại Việt Nam và khu vực.
  • Chuyển đổi công nghiệp: Phương pháp luận của luận án cung cấp giải pháp kỹ thuật trực tiếp cho các ngành công nghiệp đòi hỏi độ tin cậy phần mềm cấp độ cao như Công nghệ Tài chính (Fintech), Điều khiển Ô tô tự hành (Automotive ISO 26262), Hệ thống thông tin Y tế và Điều khiển Giao thông Vận tải Thông minh (ITS).
  • Lợi ích xã hội và chính sách: Đóng góp vào việc nâng cao năng lực kiểm định chất lượng phần mềm quốc gia, hỗ trợ xây dựng các tiêu chuẩn kiểm thử tự động cho các hạ tầng thông tin trọng yếu của chính phủ điện tử.

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

  • Nghiên cứu sinh và Giới học thuật (Academic Researchers): Tiếp cận phương pháp luận chi tiết, các công thức toán học tường minh về LTS, I/O Automata, CNNFA và thuật toán học giả định cải tiến để phát triển các đề tài nghiên cứu chuyên sâu về Formal Methods.
  • Kỹ sư Kiến trúc Phần mềm & Trưởng nhóm R&D (Software Architects & Lead Engineers): Nắm vững quy trình tự động hóa kiểm tra tính đúng đắn của bản vẽ thiết kế trước khi giao cho đội ngũ lập trình viên, loại bỏ hoàn toàn các lỗi sai kiến trúc đắt giá.
  • Chuyên gia Đảm bảo Chất lượng (QA/QC & Verification Specialists): Được trang bị tư duy và công cụ kiểm chứng mô hình hình thức tiên tiến, vượt lên trên các phương pháp kiểm thử hộp đen/hộp trắng truyền thống vốn không thể chứng minh được tính không có lỗi của phần mềm.
  • Nhà hoạch định chính sách công nghệ: Có cơ sở khoa học xác đáng để xây dựng quy chuẩn nghiệm thu phần mềm đối với các dự án công nghệ thông tin sử dụng ngân sách nhà nước có yêu cầu an toàn nghiêm ngặ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à Phương pháp sinh giả định nhỏ nhất cục bộ (Locally Minimal Assumption - $A_S$) trong kiểm chứng giả định - đảm bảo, trực tiếp mở rộng khung lý thuyết học máy tự động $L^*$ của Angluin (1987) và lý thuyết kiểm chứng thành phần của Cobleigh et al. (2003). Bằng việc sử dụng thuật toán tìm kiếm chiều rộng (BFS) trên các vết của giả định yếu nhất $A_w$, luận án tạo ra giả định $A_S$ có ngôn ngữ nhỏ hơn $\mathcal{L}(A_S) \subset \mathcal{L}(A_{org})$, giúp giả định mang tính ràng buộc chặt chẽ hơn đối với môi trường và tối ưu hóa chi phí cho kiểm chứng phần mềm tiến hóa.

2. Sự đổi mới về mặt phương pháp luận so với các nghiên cứu quốc tế trước đây thể hiện như thế nào?

So với phương pháp Thompson của Cook & Wolf (1998) và phương pháp học $L^*$ trực tiếp của Hùng et al. (2012), luận án ứng dụng thuật toán CNNFA (Chang & Paige, 1997) để chuyển đổi biểu thức chính quy trích xuất từ UML 2.0 sang LTS, giúp giảm đáng kể kích thước bộ nhớ và số lượng trạng thái trung gian. So với công trình của Barringer et al. (2011) [90], luận án đã tách biệt hoàn toàn pha sinh mô hình độc lập với pha kiểm chứng, đồng thời mở rộng mô hình ôtômát vào/ra hướng sự kiện (EDIOA) hỗ trợ đầy đủ 10 phân đoạn kết hợp phức tạp của UML 2.0.

Bảng so sánh phương pháp luận đa chiều:
+----------------------+--------------------+---------------------+----------------------+
| Đặc trưng kỹ thuật   | Cook & Wolf [27]   | Barringer et al.[90]| Luận án Lê Chí Luận  |
+----------------------+--------------------+---------------------+----------------------+
| Kỹ thuật sinh mô hình| Thuật toán Thompson| Event DFA trực tiếp | Regex -> CNNFA/EDIOA |
| Trạng thái trung gian| Rất lớn (dư thừa ε)| Trung bình          | Tối thiểu hóa (Nén)  |
| Tách biệt kiểm chứng | Không              | Không               | Có (Tái sử dụng cao) |
| Cải tiến thuật toánL*| Không áp dụng      | Không áp dụng       | Dictionary + Suffix  |
| Giả định tối thiểu   | Không              | Không               | Locally Minimal (As) |
+----------------------+--------------------+---------------------+----------------------+

3. Phát hiện bất ngờ nhất trong quá trình phân tích dữ liệu thực nghiệm là gì?

Phát hiện bất ngờ nhất là sự đánh đổi hiệu năng có chủ đích (Performance Trade-off): Để sinh ra giả định mạnh hơn ($A_S$), thuật toán phải thực hiện số lượng truy vấn ứng viên ($EQ$) nhiều hơn (ví dụ tại TestCase2, $EQ$ tăng từ 3 lên 17 lần; thời gian tăng từ 9 ms lên 43 ms). Tuy nhiên, tại các hệ thống có cấu trúc vết phức tạp (TestCase3), số lượng truy vấn thành viên lại giảm ngoạn mục từ 73 xuống 38 truy vấn ($MQ$). Sự đánh đổi này mang lại lợi ích ròng vượt trội khi hệ thống bước vào giai đoạn bảo trì và tiến hóa kiến trúc.

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 có. Luận án mô tả chi tiết kiến trúc công cụ IAGTool, cung cấp mã giả của toàn bộ 34 thuật toán thành phần (từ thuật toán sinh biểu thức chính quy cho 10 phân đoạn UML, thuật toán CNNFA, thuật toán chuyển đổi I/O Automata sang Promela, đến thuật toán cải tiến $L^*$). Toàn bộ thông số môi trường phần cứng, hệ điều hành, cấu hình bộ nhớ và các tệp đặc tả thiết kế mẫu (Testcase1.lts, Testcase2.lts, Testcase3.lts, tệp XML của hệ thống Mod2 và Ticket Booking) đều được tài liệu hóa chi tiết, cho phép tái lập chính xác kết quả thực nghiệm trên các công cụ LTSA và SPIN.

5. Chương trình nghiên cứu 10 năm tiếp theo (10-Year Research Agenda) được vạch ra như thế nào?

Chương trình nghiên cứu dài hạn tập trung vào 3 trụ cột:

  1. Mở rộng sang hệ thống thời gian thực và lai (Real-Time & Hybrid Systems): Tích hợp ngữ nghĩa thời gian (Timed Automata) vào biểu đồ tuần tự để kiểm chứng các hệ thống Cyber-Physical Systems (CPS).
  2. Kiểm chứng thành phần quy mô siêu lớn (Ultra-Large-Scale CBSD): Tự động hóa phân tách hệ thống $n$-thành phần bằng các kỹ thuật học sâu kết hợp lý thuyết đồ thị.
  3. Tự động hóa sửa lỗi thiết kế (Automated Program/Design Repair): Sử dụng phản ví dụ $cex$ không chỉ để kiểm chứng mà còn tự động sinh các bản vá lỗi (Patches) cho mô hình thiết kế UML ban đầu.

Kết luận

  1. Đóng góp 1: Xây dựng thành công phương pháp tự động trích xuất mô hình hành vi LTS từ biểu đồ tuần tự UML 2.0 thông qua cầu nối biểu thức chính quy và thuật toán ôtômát nén CNNFA, giải quyết bài toán thiếu hụt mô hình hình thức trong kiểm chứng phần mềm.
  2. Đóng góp 2: Đề xuất mô hình Ôtômát Vào/Ra hướng sự kiện (EDIOA) bảo toàn tính tương tác đối tượng của UML 2.0 và thuật toán chuyển đổi tự động sang Promela, cho phép kiểm chứng toàn diện các đặc tả an toàn và tính sống (LTL) trên công cụ kiểm chứng chuẩn quốc tế SPIN.
  3. Đóng góp 3: Đề xuất giải pháp tối ưu hóa thuật toán học máy $L^*$ trong kiểm chứng giả định - đảm bảo bằng kỹ thuật lưu trữ Dictionary và heuristic phân tích dải hậu tố $1 \dots |cex|$, loại bỏ triệt để hiện tượng lặp vô hạn và giảm tải chi phí truy vấn thành viên.
  4. Đóng góp 4: Phát triển thành công thuật toán sinh Giả định nhỏ nhất cục bộ ($A_S$), chứng minh toán học và thực nghiệm tính bao hàm ngôn ngữ $\mathcal{L}(A_S) \subseteq \mathcal{L}(A_{org})$, mở ra giải pháp kiểm chứng có độ phức tạp thấp cho phần mềm trong bối cảnh tiến hóa cấu trúc.
  5. Đóng góp 5: Cài đặt hoàn chỉnh bộ công cụ thực nghiệm IAGTool, kiểm chứng chéo thành công với các công cụ học thuật quốc tế (LTSA, SPIN) trên các tập dữ liệu chuẩn mực, khẳng định tính khả thi và độ tin cậy tuyệt đối của các đề xuất.
  6. Giá trị kế thừa dài hạn: Luận án đã đặt nền móng lý thuyết và công nghệ vững chắc cho hướng nghiên cứu Đảm bảo chất lượng phần mềm dựa trên phương pháp hình thức tại Việt Nam, thu hẹp khoảng cách giữa các tài liệu thiết kế trực quan công nghiệp và các công cụ toán học kiểm chứng tự động đỉnh cao trên thế giới.