Tổng quan về luận án

Trong kỷ nguyên phát triển của kỹ nghệ phần mềm hiện đại, phần mềm đóng vai trò huyết mạch trong các hệ thống hạ tầng trọng yếu từ tài chính, viễn thông đến điều khiển tự động và hàng không vũ trụ. Tác giả Trịnh Thanh Bình (2011) trong luận án tiến sĩ chuyên ngành Công nghệ Thông tin tại Trường Đại học Công nghệ – Đại học Quốc gia Hà Nội đã chỉ rõ: "Phần mềm ngày càng đóng vai trò quan trọng trong xã hội hiện đại... Tuy nhiên, trong nhiều hệ thống, lỗi của phần mềm gây ra các hậu quả đặc biệt nghiêm trọng, không chỉ thiệt hại về mặt kinh tế mà còn có thể làm tổn thất trực tiếp sinh mạng con người... cài đặt thực mã nguồn chương trình có thể vi phạm các ràng buộc thiết kế."

Thực trạng phát triển phần mềm tương tranh bằng ngôn ngữ Java đối mặt với nghịch lý kỹ thuật lớn: các tiến trình tương tranh tương tác phi tất định (non-deterministic) thông qua mô hình bộ nhớ chia sẻ (Java Memory Model - JMM) và cơ chế truyền thông điệp, khiến việc tái hiện lỗi cạnh tranh dữ liệu (data race), xung đột (interference) hay khóa chết (deadlock) qua kiểm thử hộp đen thông thường là bất khả thi. Các phương pháp kiểm chứng tĩnh ở pha thiết kế chưa có cơ chế chuyển giao đảm bảo tính đúng đắn xuống mã nguồn, trong khi các kỹ thuật kiểm chứng thời điểm thực thi (runtime verification) thường làm phát sinh chi phí thực thi quá mức hoặc yêu cầu chèn mã kiểm tra rải rác làm phá vỡ kiến trúc hệ thống.

Để giải quyết triệt để khoảng trống nghiên cứu này, luận án thiết lập 4 câu hỏi nghiên cứu và giả thuyết tương ứng:

  • Câu hỏi nghiên cứu 1 ($RQ_1$): Làm thế nào để mô hình hóa và kiểm chứng hình thức các ràng buộc thứ tự giữa các tiến trình tương tranh ở mức thiết kế nhằm bảo đảm tính nhất quán dữ liệu? Giả thuyết 1 ($H_1$): Việc ánh xạ các tiến trình tương tranh thành các sự kiện trong Event-B kết hợp với kỹ thuật đồng bộ hóa bằng biến logic semaphore thông qua cơ chế làm mịn (refinement) sẽ tự động hóa việc chứng minh tính bảo toàn bất biến.
  • Câu hỏi nghiên cứu 2 ($RQ_2$): Bằng cách nào có thể đặc tả và chứng minh tính đồng thuận của hệ thống đa thành phần (Multi-Component System - MCS) ở cả mức thiết kế lẫn mức mã nguồn? Giả thuyết 2 ($H_2$): Sự phân rã và kết hợp giữa Máy trừu tượng (Machine) và Ngữ cảnh (Context) trong Event-B kết hợp kiểm chứng mã bytecode qua Java PathFinder (JPF) đảm bảo hệ thống hội tụ về kết quả mong muốn sau hữu hạn bước.
  • Câu hỏi nghiên cứu 3 ($RQ_3$): Phương pháp nào giám sát sự tuân thủ giữa mã thực thi Java và giao thức tương tác thiết kế mà không làm biến dạng mã nguồn gốc? Giả thuyết 3 ($H_3$): Chuyển đổi tự động từ Máy trạng thái giao thức (Protocol State Machine - PSM) của UML và Biểu thức chính quy mở rộng sang mã khía cạnh AspectJ cho phép phát hiện vi phạm giao thức tại thời điểm chạy mà không gây phân tán mã đặc tả.
  • Câu hỏi nghiên cứu 4 ($RQ_4$): Làm thế nào để kiểm chứng các ràng buộc thời gian thực thi (timing constraints) giữa các thành phần tương tranh? Giả thuyết 4 ($H_4$): Việc đặc tả bằng Biểu đồ thời gian (Timing Diagram - TD) của UML kết hợp mã hành vi bao quanh (around advice) trong AOP cho phép đo đạc chính xác thời gian thực thi ở cấp độ nano giây để kiểm chứng sự tuân thủ giới hạn thời gian.

Luận án hình thức hóa hệ thống tương tranh thông qua định nghĩa cấu trúc: "Một hệ thống tương tranh (Concurrent system - CS) là một bộ bốn $CS = \langle Pc, Br, \alpha, \Gamma \rangle$. Trong đó: $Pc$ là tập hữu hạn các tiến trình, $Br$ là tập hữu hạn các hành vi có thể trong $CS$, $\alpha: Br \to Pc$ hàm gán mỗi chức năng của $CS$ mà tiến trình thực hiện hành vi đó, $\Gamma$ là giao thức tương tác đặc tả thứ tự thực hiện của các tiến trình." Phạm vi nghiên cứu bao quát toàn diện vòng đời phát triển từ mô hình hóa toán học trên công cụ RODIN, phân tích mã nguồn bytecode Java bằng JPF, đến phát triển công cụ sinh mã tự động PVG (Protocol Verification Generator) tích hợp trên Eclipse và NetBeans.

Literature Review và Positioning

Tổng quan y văn quốc tế về kiểm chứng hệ thống tương tranh được chia thành hai nhánh tiếp cận chính với những ưu nhược điểm và tranh luận học thuật sâu sắc:

                      ┌───────────────────────────────────────────────┐
                      │ TIẾP CẬN KIỂM CHỨNG CHƯƠNG TRÌNH TƯƠNG TRANH  │
                      └──────────────────────┬────────────────────────┘
                                             │
             ┌───────────────────────────────┴───────────────────────────────┐
             ▼                                                               ▼
┌─────────────────────────┐                                     ┌─────────────────────────┐
│   KIỂM CHỨNG THIẾT KẾ   │                                     │   KIỂM CHỨNG MÃ NGUỒN   │
└────────────┬────────────┘                                     └────────────┬────────────┘
             │                                                               │
     ┌───────┴───────┐                                               ┌───────┴───────┐
     ▼               ▼                                               ▼               ▼
┌─────────┐     ┌─────────┐                                     ┌─────────┐     ┌─────────┐
│ Edmunds │     │  Yang   │                                     │ Bodden  │     │   Jin   │
│ (2008)  │     │ (2009)  │                                     │ (2008)  │     │ (2010)  │
│  [OCB]  │     │ [B+CSP] │                                     │[AspectJ]│     │ [CFG]   │
└─────────┘     └─────────┘                                     └─────────┘     └─────────┘

Trong hướng tiếp cận kiểm chứng thiết kế, Edmunds (2008) đề xuất ngôn ngữ trung gian OCB (Object-oriented Concurrent-B) nhằm che giấu cơ chế khóa (locking) và khối (blocking), ánh xạ các mệnh đề nguyên tử được gán nhãn vào máy Event-B. Tuy nhiên, OCB gặp giới hạn khi chuyển đổi sang mã Java thực tế vì không kiểm soát được các hành vi tương tác động phức tạp phát sinh từ môi trường máy ảo. Ben Younes và cộng sự (2010) phát triển các luật chuyển đổi từ Biểu đồ hoạt động (Activity Diagram) của UML sang Event-B để kiểm chứng tính công bằng (fairness) và khóa chết, nhưng quy trình chưa tự động hóa hoàn toàn và dừng lại ở các ví dụ minh họa đơn giản. Ball (2008) đưa ra các mẫu thiết kế tương tác tác tử chuyển sang Event-B nhưng thiếu vắng công cụ tự động hóa. Yang (2009) kết hợp CSP (Communicating Sequential Processes của Hoare) và B-Method trong công cụ PROB để sinh mã Java/JCSPRO; phương pháp này chặt chẽ nhưng áp đặt một mô hình lập trình tương tranh hạn hẹp, khó áp dụng cho các cấu trúc Java tiêu chuẩn.

Ở hướng tiếp cận kiểm chứng mã nguồn, Bodden (2005) phát triển công cụ J-LO (Java Logical Observer) sử dụng logic thời gian tuyến tính (LTL) và trình biên dịch AspectBench để bắt lỗi hạt giống (seeded errors), nhưng chi phí thời gian thực thi (runtime overhead) bùng nổ khiến công cụ chỉ dùng được trên các chương trình quy mô nhỏ. Bodden và Havelund (2008) mở rộng AspectJ với các phương thức lock(), unlock(), maybeShare() để phát hiện cạnh tranh dữ liệu (data race), song bỏ ngỏ các lỗi bế tắc (deadlock) và vi phạm giao thức đa thành phần. Jin (2010) ứng dụng văn phạm phi ngữ cảnh (CFG) qua công cụ Accent để kiểm chứng tĩnh chuỗi gọi phương thức (Method Call Sequence - MCS) trên ôtômát hữu hạn trạng thái $L(G) \subseteq L(A)$, nhưng phương pháp này chỉ giải quyết được chương trình Java tuần tự và vấp phải bài toán phức tạp về độ bao phủ ngôn ngữ (language inclusion problem). Tiếp cận bằng JML (Java Modeling Language của Leavens và cộng sự) yêu cầu viết tiền/hậu điều kiện và bất biến lồng ghép trong thân hàm, dẫn đến hiện tượng mã kiểm tra bị phân tán, khó bảo trì và không tách biệt được mối quan tâm về giao thức.

Luận án của Trịnh Thanh Bình định vị chính xác khoảng trống học thuật: thiết lập một cầu nối xuyên suốt hai chiều giữa kiểm chứng hình thức mức mô hình (thông qua chứng minh định lý bằng Event-B) và kiểm chứng thực nghiệm mức mã nguồn (thông qua kiểm chứng mô hình JPF và thực thi cắt ngang bằng AOP/AspectJ). Nghiên cứu giải quyết đồng thời cả 4 khía cạnh: ràng buộc thứ tự tiến trình, sự đồng thuận đa thành phần, sự tuân thủ giao thức tương tác và ràng buộc thời gian thực thi.

Đó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 phương pháp hình thức Event-B của Jean-Raymond Abrial (2010) và Lý thuyết Logic Hoare (1969) vào miền bài toán lập trình tương tranh hướng đối tượng:

  1. Hình thức hóa cơ chế đồng bộ hóa luồng trong Event-B: Mở rộng lý thuyết máy chuyển trạng thái trừu tượng bằng cách đưa biến logic đóng vai trò semaphore điều khiển thứ tự thực thi của các sự kiện có biểu thức bảo vệ (guards) không rời nhau ($G_1 \cap G_2 \cap \dots \cap G_n \neq \emptyset$), đảm bảo tính đúng đắn khi thực thi đan xen (interleaving).
  2. Lý thuyết về sự đồng thuận của hệ thống đa thành phần (MCS): Xây dựng các bổ đề toán học và mô hình hóa tính dừng, tính an toàn của hệ thống tương tranh đa tác tử dựa trên quan hệ giữa Máy thực thi và Ngữ cảnh tĩnh.
  3. Mở rộng lý thuyết Logic thời gian và Thực thi cắt ngang (Crosscutting Semantics): Ánh xạ ngữ nghĩa của Máy trạng thái giao thức (PSM) và Biểu đồ thời gian (TD) sang ngữ nghĩa điểm nối (joinpoints), hướng cắt (pointcuts) và mã hành vi (advices) trong mô hình AOP của Gregor Kiczales.

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

Khung phân tích của luận án tích hợp đa tầng ba lý thuyết nền tảng: Lý thuyết tập hợp & Logic vị từ bậc một (Set Theory & First-Order Logic trong Event-B), Cấu trúc Kripke & Logic thời gian (Kripke Structures & Temporal Logic LTL/CTL), và Lý thuyết tách biệt các mối quan tâm (Separation of Concerns trong AOP).

graph TD
    subgraph DesignLevel["TẦNG MÔ HÌNH THIẾT KẾ (Design Level)"]
        A["Mô hình Trừu tượng Event-B (Abstract Machine & Context)"] -->|Làm mịn Refinement| B["Mô hình Làm mịn (Refined Machine với Semaphores)"]
        B -->|Proof Obligations Generator| C["Chứng minh Định lý Tự động (RODIN Prover)"]
        D["Đặc tả UML 2.0 (Sequence, PSM, Timing Diagrams)"] -->|Hình thức hóa| B
    end

    subgraph Bridge["CÔNG CỤ CẦU NỐI (PVG Tool)"]
        C -->|Sinh mã khía cạnh| E["AspectJ Aspects Generation"]
        D -->|Sinh mã kiểm chứng| E
    end

    subgraph ImplementationLevel["TẦNG MÃ NGUỒN & THỰC THI (Implementation Level)"]
        E -->|Đan mã Weaving| F["Java Bytecode Integration"]
        G["Chương trình Java Tương tranh (Java Threads/JMM)"] -->|Biên dịch| F
        F -->|Kiểm chứng mô hình Bytecode| H["Java PathFinder (JPF Search & VM Listeners)"]
        F -->|Kiểm chứng thời điểm chạy| I["Runtime Verification (Sai số nano giây)"]
    end

Khung phân tích thiết lập điều kiện biên (boundary conditions) chặt chẽ:

  • Tầng tĩnh (Static/Design Phase): Không gian trạng thái được thu hẹp thông qua cơ chế phân rã (decomposition) và làm mịn (refinement), triệt tiêu nguy cơ bùng nổ không gian trạng thái trước khi chuyển giao mã.
  • Tầng động (Dynamic/Runtime Phase): Đặc tả giao thức được module hóa hoàn toàn bên trong các khía cạnh (aspects), cô lập hoàn toàn khỏi mã nghiệp vụ Java, loại bỏ rủi ro tạo lỗi phụ (side-effects) trên luồng dữ liệu gốc.

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ủ chặt chẽ thế giới quan thực chứng (positivism) kết hợp phương pháp luận diễn dịch hình thức (formal-deductive methodology). Thiết kế nghiên cứu đa tầng kết hợp giữa chứng minh toán học tiên đề (axiomatic proof) và thực nghiệm mô phỏng máy ảo chuyên sâu:

  • Mức độ 1 (Thiết kế & Toán học): Sử dụng logic bậc một để sinh các mệnh đề chứng minh bảo toàn bất biến ($inv$) và tính khả định nghĩa của sự kiện.
  • Mức độ 2 (Mã nguồn Bytecode): Sử dụng bộ kiểm chứng mô hình JPF duyệt không gian trạng thái thực thi trên máy ảo Java ảo chuyên biệt.
  • Mức độ 3 (Thời gian thực thi): Ứng dụng kỹ thuật kiểm thử bị động (passive runtime verification) đo lường độ trễ và sự tuân thủ giao thức.

Quy trình nghiên cứu rigorous

Quy trình kiểm chứng hình thức tại mức thiết kế được tự động hóa qua luật sinh mệnh đề cần chứng minh (Proof Obligations - PO) trong Event-B:

$$\frac{A(s, c) \quad I(s, c, v) \quad G(s, c, v, x) \quad BA(s, c, v, x, v')}{inv(s, c, v')}$$

Trong đó: $A(s, c)$ là tập tiên đề và định lý trong Ngữ cảnh; $I(s, c, v)$ là các bất biến trong Máy; $G(s, c, v, x)$ là biểu thức điều kiện bảo vệ của sự kiện; $BA(s, c, v, x, v')$ là vị từ quan hệ trước-sau; $inv(s, c, v')$ là bất biến được làm mịn cần chứng minh bảo toàn.

┌─────────────────────────────────────────────────────────────────────────┐
│                  QUY TRÌNH KIỂM CHỨNG TOÀN DIỆN                         │
└────────────────────────────────────┬────────────────────────────────────┘
                                     │
         ┌───────────────────────────┴───────────────────────────┐
         ▼                                                       ▼
┌─────────────────────────────────┐     ┌─────────────────────────────────┐
│     TẦNG THIẾT KẾ (EVENT-B)     │     │     TẦNG MÃ NGUỒN (AOP & JPF)   │
├─────────────────────────────────┤     ├─────────────────────────────────┤
│ • Đặc tả máy trừu tượng         │     │ • Xây dựng mã Java tương tranh  │
│ • Bổ sung biến semaphore        │     │ • Mở rộng JPF VMListener        │
│ • Áp dụng cơ chế làm mịn        │     │ • Tự động sinh mã AspectJ (PVG) │
│ • Sinh Proof Obligations (PO)   │     │ • Đan mã vào Bytecode           │
│ • Chứng minh tự động qua RODIN  │     │ • Giám sát thực thi nano giây   │
└─────────────────────────────────┘     └─────────────────────────────────┘

Tại tầng thực thi mã nguồn, luận án phát triển công cụ PVG (Protocol Verification Generator) thực hiện chuyển đổi tự động từ biểu đồ PSM và biểu thức chính quy sang các thành phần AspectJ:

  • Khai báo Điểm nối (Joinpoints): Xác định chính xác method call joinpoint và method execution joinpoint.
  • Định nghĩa Hướng cắt (Pointcuts): Tạo hướng cắt đại diện cho các sự kiện giao thức, ví dụ: 
    pointcut pc_init(Applet o): target(o) && call(void init());
  • Mã hành vi (Advices): Sử dụng before advice để kiểm tra trạng thái tiền điều kiện, after advice để chuyển đổi trạng thái giao thức, và around advice sử dụng hàm proceed() cùng System.nanoTime() để bao đóng và đo thời gian thực thi.
  • Mở rộng JPF Listener: Cài đặt hai giao diện cốt lõi của JPF là SearchListener (theo dõi đường tìm kiếm trạng thái) và VMListener (bắt sự kiện chỉ thị bytecode instructionExecuted).

Data và phân tích

Dữ liệu kiểm chứng được xây dựng trên hệ thống các ca kiểm thử và mô hình bài toán kinh điển chuẩn hóa quốc tế:

  1. Bài toán Vùng xung đột (Critical Section Problem): Mô hình hóa $n$ tiến trình truy cập tài nguyên dùng chung qua biến semaphore turn \in NAT.
  2. Bài toán Cung cấp - Tiêu thụ (Producer - Consumer Problem): Đánh giá trên mô hình đa tiến trình với $n$ tiến trình Producer và $m$ tiến trình Consumer cùng bộ đệm hữu hạn (Buffer Size), kiểm soát qua các biến semaphore Count, TurnP \in Producers, TurnC \in Consumers, và cờ logic isClose.
  3. Bài toán Đọc - Ghi (Reader - Writer Problem): Kiểm chứng tính nhất quán dữ liệu bộ nhớ chia sẻ.
  4. Hệ thống Đa thành phần tính toán số học nhị phân: Kiểm chứng 4 thành phần phối hợp: phép dịch bit (BitShift), nhân xâu nhị phân với một bit, cộng hai xâu nhị phân, và nhân hai xâu nhị phân đa thành phần.
  5. Giao thức giao dịch tài chính ATM & Hàng đợi tương tranh: Kiểm chứng ràng buộc thời gian với biên độ ngặt nghèo trong phương thức rút tiền withdraw với ràng buộc thực thi $[726082, 1436580]$ nano giây.

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

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

Nghiên cứu mang lại 4 kết quả thực nghiệm và lý thuyết mang tính đột phá:

┌─────────────────────────────────────────────────────────────────────────┐
│                      KẾT QUẢ ĐỘT PHÁ CỦA LUẬN ÁN                        │
└────────────────────────────────────┬────────────────────────────────────┘
                                     │
         ┌───────────────────────────┼───────────────────────────┐
         ▼                           ▼                           ▼
┌──────────────────┐       ┌──────────────────┐       ┌──────────────────┐
│ TỰ ĐỘNG HÓA 100% │       │ PHÁT HIỆN LỖI SỚM│       │ ĐO ĐẠC NANO GIÂY │
├──────────────────┤       ├──────────────────┤       ├──────────────────┤
│ Chứng minh thành │       │ Bắt lỗi vi phạm  │       │ Kiểm chứng chính │
│ công các mệnh đề │       │ giao thức động   │       │ xác ràng buộc    │
│ PO trên RODIN    │       │ không cần sửa mã │       │ [726082, 1436580]│
└──────────────────┘       └──────────────────┘       └──────────────────┘
  1. Khả năng tự động hóa chứng minh định lý đạt tỷ lệ tuyệt đối: Trong bài toán ràng buộc thứ tự tiến trình và sự đồng thuận hệ thống nhị phân, 100% các mệnh đề cần chứng minh (Proof Obligations) liên quan đến tính bất biến ($inv$) và tính bảo toàn trạng thái của các sự kiện (như ShiftLeftIf, Producer, Consumer) đều được hệ thống RODIN chứng minh tự động hoàn toàn mà không cần can thiệp chứng minh thủ công (interactive proof).
  2. Triệt tiêu hoàn toàn sự phụ thuộc không gian trạng thái ở pha thiết kế: Bằng việc sử dụng kỹ thuật làm mịn từ máy trừu tượng sang máy cụ thể với các biến semaphore logic, mô hình thiết kế loại bỏ được các nhánh thực thi dẫn tới khóa chết (deadlock) hoặc cạnh tranh dữ liệu (data race) ngay từ trước khi viết mã nguồn.
  3. Phát hiện lỗi vi phạm giao thức với độ phức tạp can thiệp mã nguồn bằng 0 (Zero-invasive Instrumentation): Khác biệt hoàn toàn với JML (đòi hỏi chèn mã điều kiện rải rác vào từng phương thức), kỹ thuật sinh mã khía cạnh AspectJ từ công cụ PVG cho phép tách rời 100% mã kiểm chứng khỏi mã nguồn nghiệp vụ Java. Thực nghiệm kiểm chứng sự tuân thủ giao thức trên các ca kiểm thử đúng/sai chứng minh AspectJ bắt chính xác mọi vi phạm thứ tự gọi hàm ngay khi sự kiện xảy ra.
  4. Kiểm soát chính xác ràng buộc thời gian ở độ phân giải nano giây: Phương pháp sử dụng Biểu đồ thời gian (Timing Diagram) sinh mã around advice đã kiểm chứng thành công các ca kiểm thử thời gian thực. Ví dụ, trong phương thức withdraw của giao thức ATM, hệ thống phát hiện chính xác các vi phạm vượt ngưỡng trên ($> 1436580\text{ ns}$) hoặc vi phạm ngưỡng dưới ($< 726082\text{ ns}$) mà không làm sai lệch luồng thực thi của máy ảo Java.

Implications đa chiều

  • Về mặt lý thuyết phần mềm: Cung cấp phương pháp luận hình thức hoàn chỉnh để chuyển giao các đặc tả toán học trừu tượng sang các cấu trúc lập trình hướng đối tượng tương tranh thực tế, mở rộng năng lực biểu diễn của Event-B sang các hệ thống hướng khía cạnh.
  • Về mặt phương pháp luận kiểm định: Thiết lập quy trình kiểm thử bị động (passive runtime testing) kết hợp kiểm chứng mô hình bytecode (JPF), cung cấp chuẩn mực mới cho quy trình kiểm thử phần mềm tương tranh phức tạp.
  • Về mặt ứng dụng thực tiễn: Công cụ PVG được tích hợp trực tiếp vào môi trường phát triển NetBeans và Eclipse giúp các kỹ sư phần mềm công nghiệp dễ dàng đặc tả giao thức tương tác bằng UML trực quan và tự động sinh mã giám sát, giảm thiểu trên 80% thời gian cấu hình và viết mã kiểm thử tương tranh thủ công.
  • Về mặt chính sách và tiêu chuẩn chất lượng: Định hình tiêu chuẩn đánh giá an toàn phần mềm cho các hệ thống nhúng, giao dịch ngân hàng và điều khiển thời gian thực tại Việt Nam và quốc tế.

Limitations và Future Research

Nhìn nhận một cách khách quan và khoa học, luận án tồn tại một số giới hạn nghiên cứu:

  1. Giới hạn bùng nổ không gian trạng thái trong JPF: Khi số lượng tiến trình tương tranh ($n, m$) tăng lên quy mô lớn trong các ứng dụng phân tán phức tạp, công cụ JPF vẫn gặp hiện tượng tiêu tốn bộ nhớ khi duyệt toàn bộ không gian trạng thái bytecode.
  2. Độ trễ do cơ chế đan mã AspectJ (Instrumentation Overhead): Việc chèn mã hành vi xung quanh (around advice) để thu thập dữ liệu thời gian nano giây dù rất nhỏ nhưng vẫn tạo ra một độ trễ nhất định, có thể ảnh hưởng nhẹ đến các hệ thống thời gian thực siêu ngặt nghèo (hard real-time systems).
  3. Mức độ tự động hóa trong các cấu trúc dữ liệu phi tuyến tính: Đối với các bài toán có bất biến phi tuyến tính phức tạp, bộ sinh mệnh đề của RODIN đôi khi vẫn cần sự can thiệp của chuyên gia để định hướng chứng minh bổ đề.

Chương trình nghiên cứu 10 năm tiếp theo (Future Research Agenda):

  • Tích hợp kỹ thuật thực thi ký hiệu (Symbolic Execution) vào JPF nhằm giảm không gian tìm kiếm trạng thái.
  • Mở rộng phương pháp kiểm chứng sang các mô hình lập trình tương tranh phân tán hiện đại như Actor Model trong Akka, mô hình bất biến trong Rust và điện toán đám mây đa lõi.
  • Tự động hóa việc suy diễn và sinh bất biến (Invariant Generation) từ mã nguồn Java ngược lên mô hình Event-B (Reverse Engineering).

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

Luận án của Trịnh Thanh Bình đã tạo ra tiếng vang học thuật và giá trị ứng dụng rõ rệt:

┌─────────────────────────────────────────────────────────────────────────┐
│                    TÁC ĐỘNG VÀ GIÁ TRỊ THỰC TIỄN                        │
└────────────────────────────────────┬────────────────────────────────────┘
                                     │
         ┌───────────────────────────┴───────────────────────────┐
         ▼                                                       ▼
┌─────────────────────────────────┐     ┌─────────────────────────────────┐
│        GIÁ TRỊ HỌC THUẬT        │     │       ỨNG DỤNG CÔNG NGHIỆP      │
├─────────────────────────────────┤     ├─────────────────────────────────┤
│ • Công bố trên các kỷ yếu và tạp│     │ • Tích hợp công cụ PVG trên IDE │
│   chí chuyên ngành uy tín       │     │   phổ biến (Eclipse, NetBeans)  │
│ • Tiên phong kết hợp Event-B,   │     │ • Ứng dụng kiểm thử hệ thống lõi│
│   UML 2.0, AOP và JPF tại VN    │     │   ngân hàng, tài chính, viễn    │
│ • Tài liệu chuẩn cho đào tạo    │     │   thông và điều khiển tự động   │
│   sau đại học về Formal Methods │     │ • Giảm chi phí gỡ lỗi tương     │
│                                 │     │   tranh trong vòng đời phần mềm │
└─────────────────────────────────┘     └─────────────────────────────────┘

Nghiên cứu tiên phong tại Việt Nam trong việc kết hợp nhuần nhuyễn giữa phương pháp hình thức hàn lâm và công nghệ phần mềm thực nghiệm, cung cấp giải pháp giảm thiểu chi phí phát hiện và sửa lỗi tương tranh trong các dự án công nghiệp phần mềm quy mô lớn.

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

  • Nghiên cứu sinh & Nhà khoa học chuyên ngành Công nghệ Phần mềm: Tiếp cận mô hình toán học mẫu mực về việc ứng dụng Event-B và cơ chế làm mịn để giải quyết bài toán tương tranh phức tạp; kế thừa khung lý thuyết để mở rộng sang các hệ thống phân tán.
  • Kiến trúc sư phần mềm & Chuyên gia R&D công nghiệp: Ứng dụng quy trình thiết kế và công cụ PVG để đặc tả kiến trúc tương tác chuẩn mực cho các hệ thống giao dịch ngân hàng, viễn thông và phần mềm nhúng.
  • Kỹ sư Đảm bảo Chất lượng (QA/QC Engineers): Nắm vững kỹ thuật kiểm chứng thời điểm thực thi bằng AspectJ và JPF để tự động hóa quy trình phát hiện lỗi cạnh tranh dữ liệu và vi phạm giao thức mà không cần viết test suite thủ công phức tạp.
  • Cơ quan Quản lý Tiêu chuẩn & An toàn Hệ thống: Sử dụng phương pháp kiểm chứng hình thức làm căn cứ thẩm định mức độ tin cậy và an toàn của các phần mềm thuộc hạ tầng trọng yếu quốc gia.

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 mở rộng Lý thuyết Làm mịn (Refinement Theory) trong Event-B của Abrial sang việc kiểm soát thứ tự thực thi của các tiến trình tương tranh hướng đối tượng. Tác giả đã giải quyết nghịch lý giữa tính trừu tượng phi thời gian của Event-B và tính thực thi đan xen phụ thuộc thời gian của luồng Java bằng cách đưa biến trạng thái semaphore logic vào biểu thức bảo vệ (guards). Điều này cho phép bảo toàn bất biến an toàn và loại trừ tương tranh hoàn toàn ở cấp độ toán học trước khi cài đặt.

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

So với nghiên cứu của Edmunds (2008) trên ngôn ngữ trung gian OCB và Bodden & Havelund (2008) trên AspectJ mở rộng:

  • Edmunds chỉ dừng lại ở việc sinh mã Java từ OCB mà không có cơ chế giám sát kiểm tra tính tuân thủ khi mã Java chạy trong môi trường JVM thực tế.
  • Bodden & Havelund chỉ bắt được lỗi cạnh tranh dữ liệu ở mức biến đơn lẻ, không kiểm chứng được tính đúng đắn của toàn bộ giao thức tương tác đa thành phần và ràng buộc thời gian.
  • Luận án của Trịnh Thanh Bình là công trình đầu tiên thiết lập quy trình khép kín 2 chiều: Đặc tả & Chứng minh thiết kế (Event-B/RODIN) $\rightarrow$ Mô hình hóa trực quan (UML PSM/TD) $\rightarrow$ Tự động sinh mã giám sát độc lập (PVG/AspectJ) $\rightarrow$ Kiểm chứng mô hình bytecode (JPF).

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

Phát hiện bất ngờ nhất là tính khả thi của việc giám sát chính xác ràng buộc thời gian ở cấp độ nano giây thông qua mã khía cạnh bao quanh (around advice) mà không làm méo mó ngữ nghĩa thực thi của ứng dụng Java. Việc kết hợp giữa Biểu đồ thời gian (Timing Diagram) và AspectJ đã phát hiện chính xác các vi phạm khoảng thời gian $[726082, 1436580]\text{ ns}$ trong phương thức rút tiền ATM, chứng minh rằng AOP hoàn toàn đủ năng lực phục vụ kiểm chứng thời gian thực mềm (soft real-time) mà không cần can thiệp vào mã nguồn máy ảo JVM.

4. Luận án có cung cấp giao thức tái lập (Replication Protocol) không?

Có. Luận án cung cấp chi tiết toàn bộ mã đặc tả máy Event-B trong các Phụ lục A, B (cho bài toán Vùng xung đột, Cung cấp - Tiêu thụ, Đọc - Ghi, và Hệ thống phép toán nhị phân), cấu hình bộ công cụ RODIN, cùng kiến trúc và mã nguồn công cụ sinh mã PVG trong Phụ lục C với giao diện tích hợp trên NetBeans/Eclipse, cho phép cộng đồng học thuật tái lập 100% các kết quả thực nghiệm.

5. Lộ trình phát triển học thuật 10 năm được phác thảo như thế nào?

Lộ trình hướng tới việc tự động hóa toàn diện quy trình kiểm chứng phần mềm tự trị (Autonomous Software Verification): tích hợp kiểm chứng hình thức vào quy trình CI/CD hiện đại, mở rộng công cụ PVG để hỗ trợ các ngôn ngữ đa luồng thế hệ mới (Go, Rust, Scala), và ứng dụng trí tuệ nhân tạo để tự động trích xuất mô hình đặc tả từ hành vi thực thi phân tán.

Kết luận

Luận án tiến sĩ của Trịnh Thanh Bình (2011) là một công trình khoa học mẫu mực, giải quyết trọn vẹn bài toán kiểm chứng các thành phần Java tương tranh với 5 đóng góp cốt lõi:

  1. Phương pháp luận kiểm chứng toàn diện: Kết hợp thành công giữa kiểm chứng tĩnh mức mô hình thiết kế (Event-B) và kiểm chứng động mức cài đặt mã nguồn (AOP, JPF).
  2. Mô hình hóa hình thức ràng buộc thứ tự và sự đồng thuận: Giải quyết triệt để các bài toán tương tranh kinh điển (Critical Section, Producer-Consumer, Reader-Writer, Multi-Component Arithmetic) bằng chứng minh định lý toán học tự động trên RODIN.
  3. Kỹ thuật kiểm chứng giao thức tương tác không xâm lấn: Ứng dụng xuất sắc AOP (AspectJ) để giám sát sự tuân thủ giữa thực thi và đặc tả PSM mà không làm phân tán mã nguồn.
  4. Kiểm chứng ràng buộc thời gian chính xác cao: Tiên phong ứng dụng Biểu đồ thời gian của UML và mã khía cạnh để kiểm tra giới hạn thời gian ở cấp độ nano giây.
  5. Công cụ thực nghiệm PVG hoàn chỉnh: Chuyển giao trực tiếp kết quả nghiên cứu lý thuyết thành công cụ phần mềm ứng dụng thực tế tích hợp trên các IDE tiêu chuẩn công nghiệp.

Công trình không chỉ đặt nền móng vững chắc cho hướng nghiên cứu phương pháp hình thức ứng dụng tại Việt Nam mà còn đóng góp giải pháp kỹ thuật có giá trị tham khảo lâu dài cho nền kỹ nghệ phần mềm quốc tế.