Tổng quan luận án

Trong kỹ nghệ phần mềm, công nghệ phần mềm dựa trên thành phần (Component-Based Software Engineering - CBSE) được ứng dụng rộng rãi nhằm nâng cao hiệu quả phát triển, giảm thiểu chi phí và tăng khả năng bảo trì hệ thống. Đối với các hệ thống phần mềm có yêu cầu cao về độ tin cậy như hệ thống điều khiển trong ô tô, tàu hỏa, hàng không vũ trụ hay các thiết bị Internet vạn vật (IoT), việc bảo đảm các thuộc tính an toàn (safety properties) trong suốt quá trình vận hành là yêu cầu bắt buộc. Hai hướng tiếp cận chính để giải quyết bài toán này gồm chứng minh định lý (theorem proving) và kiểm chứng mô hình (model checking). Trong đó, kiểm chứng mô hình là phương pháp tự động hoàn toàn nhưng gặp phải thách thức lớn về sự bùng nổ không gian trạng thái (state space explosion) khi quy mô hệ thống tăng lên.

Phương pháp kiểm chứng giả định - đảm bảo (Assume-Guarantee Verification - AGV) dựa trên nguyên lý chia để trị đã được đề xuất nhằm giải quyết vấn đề bùng nổ không gian trạng thái. Hệ thống tổng thể gồm nhiều thành phần được chia nhỏ để kiểm chứng độc lập mà không cần phải ghép nối toàn bộ các thành phần lại với nhau. Tuy nhiên, các kỹ thuật kiểm chứng giả định - đảm bảo hiện tại vẫn bộc lộ những hạn chế về chi phí thời gian tính toán và khả năng áp dụng khi phần mềm tiến hóa. Cụ thể, các thuật toán sinh giả định hiện có cho hệ thống chuyển trạng thái được gán nhãn (LTS) chưa tối ưu được kích thước và ngôn ngữ của giả định; các kỹ thuật kiểm chứng trên mô hình lôgic mệnh đề buộc phải sinh lại giả định từ đầu trong mọi trường hợp khi có sự thay đổi của thành phần; và các quy trình kiểm chứng hai pha cho hệ thống có ràng buộc thời gian (ERA) còn phức tạp, khó triển khai trong thực tế.

Luận án xác định 3 mục tiêu nghiên cứu cụ thể như sau:

  1. Mục tiêu thứ nhất: Sinh giả định nhỏ nhất và mạnh nhất cho bài toán kiểm chứng giả định - đảm bảo đối với phần mềm đặc tả bằng hệ chuyển trạng thái được gán nhãn (LTS), nhằm giảm chi phí thời gian khi sinh lại giả định trong quá trình kiểm chứng phần mềm đã tiến hóa.
  2. Mục tiêu thứ hai: Giảm chi phí thời gian của quá trình kiểm chứng giả định - đảm bảo phần mềm đã tiến hóa bằng cách giảm số lần sinh lại giả định khi kiểm chứng hồi quy đối với phần mềm đặc tả bằng lôgic mệnh đề, thông qua phương pháp sinh giả định yếu nhất cục bộ.
  3. Mục tiêu thứ ba: Tiến hành thử nghiệm cài đặt phiên bản một pha cho phương pháp kiểm chứng giả định - đảm bảo hai pha đối với phần mềm có ràng buộc thời gian đặc tả bằng ô-tô-mát ghi sự kiện (ERA), đồng thời xử lý các vấn đề phát sinh trong quá trình cài đặt thực tế.

Đối tượng và phạm vi nghiên cứu của luận án:

  • Đối tượng nghiên cứu: Các phương pháp và thuật toán kiểm chứng giả định - đảm bảo tự động cho phần mềm dựa trên thành phần.
  • Phạm vi nghiên cứu: Luận án tập trung vào các hệ thống phần mềm tương tranh không có ràng buộc thời gian và có ràng buộc thời gian; thuộc tính kiểm chứng là thuộc tính an toàn; các mô hình hình thức bao gồm hệ chuyển trạng thái được gán nhãn (LTS), hệ thống chuyển trạng thái đặc tả bằng lôgic mệnh đề, và ô-tô-mát ghi sự kiện (ERA) trong cả hai ngữ cảnh kiểm chứng ban đầu và kiểm chứng hồi quy khi phần mềm tiến hóa.

Tổng quan tài liệu và vị trí của luận án

Luận án tiến hành khảo cứu có hệ thống các công trình nghiên cứu về kiểm chứng hình thức, chia theo các nhóm tiếp cận và mô hình đặc tả:

  1. Hướng tiếp cận kiểm chứng mô hình và kiểm chứng giả định - đảm bảo nền tảng: Kiểm chứng mô hình tự động được đặt nền móng bởi Clarke, Emerson và Sifakis [12, 24, 25, 27, 54, 90]. Để giải quyết bùng nổ không gian trạng thái, kiểm chứng giả định - đảm bảo được Pnueli, Clarke, Long, McMillan đề xuất và phát triển [23, 44, 52, 81, 88]. Các phương pháp lập luận được phân thành hai nhóm: lập luận quay vòng (Circular Assume - Guarantee Reasoning - CIRC-AG) [3, 64, 75, 77, 78, 84] và lập luận không quay vòng (Non-Circular Assume - Guarantee Reasoning - NC-AG) [5, 21, 23, 41, 44, 68, 76, 96].

  2. Kiểm chứng giả định - đảm bảo cho hệ thống đặc tả bằng LTS: Giannakopoulou và cộng sự chứng minh sự tồn tại của giả định yếu nhất (Weakest Assumption - $A_W$) [41, 87]. Cobleigh và cộng sự áp dụng thuật toán học ngôn ngữ chính quy $L^*$ của Angluin [8] và Rivest - Schapire [91] để tự động sinh giả định [29]. Sau đó, nhiều nghiên cứu mở rộng và tối ưu phương pháp của Cobleigh: Chaki và Strichman đề xuất tối thiểu hóa bảng chữ cái của giả định [18, 19]; Gupta và cộng sự áp dụng bộ giải SAT và kỹ thuật lấy mẫu cho hệ thống phần cứng [46]; Phạm Ngọc Hùng và cộng sự đề xuất phương pháp sinh giả định có kích thước nhỏ nhất dựa trên thuật toán tìm kiếm theo chiều sâu (DFS) và tìm kiếm theo chiều sâu có giới hạn [55, 56, 57, 58, 86]; He và cộng sự mở rộng cho hệ thống xác suất Markov bằng sơ đồ quyết định nhị phân đa chiều (MTBDD) [47]; Bensalem và cộng sự áp dụng bất biến hệ thống trên ngôn ngữ BIP [11]; Abbasi và cộng sự nghiên cứu kiểm chứng hệ thống không đồng bộ có thành phần chưa xác định [1].

  3. Kiểm chứng giả định - đảm bảo cho hệ thống đặc tả bằng lôgic mệnh đề: Sinha và cộng sự sử dụng bộ giải SAT cho hệ thống đặc tả bằng lôgic mệnh đề [94]. Chen và cộng sự áp dụng thuật toán học hàm lôgic CDNF (Conjunction of Disjunctive Normal Form) của Bshouty [15] vào kiểm chứng giả định - đảm bảo [21]. Tiếp đó, He và cộng sự tối ưu thuật toán sinh giả định dựa trên CDNF cho kiểm chứng hồi quy [48].

  4. Kiểm chứng giả định - đảm bảo cho hệ thống có ràng buộc thời gian: Alur và Dill đề xuất ô-tô-mát ghi sự kiện (Event-Recording Automata - ERA) [4]. Grinchtein và cộng sự phát triển thuật toán học $TL^_{sg}$ [42]. Lin và cộng sự mở rộng thành thuật toán $TL^$, tích hợp vào bộ công cụ PAT [71, 97] và đề xuất quy trình kiểm chứng hai pha cho hệ thống có ràng buộc thời gian [68, 69].

Khoảng trống nghiên cứu luận án lựa chọn giải quyết:

  • Trong mô hình LTS: Thuật toán của Cobleigh và cộng sự dựa trên ngôn ngữ của giả định yếu nhất $L(A_W)$ và dừng ngay khi tìm được kết quả, do đó giả định sinh ra chưa phải là mạnh nhất. Các nghiên cứu của Phạm Ngọc Hùng và cộng sự mới chỉ tập trung vào việc giảm số trạng thái (kích thước) mà chưa tối ưu hóa độ lớn ngôn ngữ của giả định. Luận án giải quyết khoảng trống này bằng cách đề xuất phương pháp sinh giả định vừa nhỏ nhất vừa mạnh nhất cục bộ.
  • Trong mô hình lôgic mệnh đề: Phương pháp của He và cộng sự vẫn yêu cầu sinh lại giả định trong tất cả các trường hợp khi phần mềm tiến hóa, ngay cả khi thành phần chỉ có thay đổi nhỏ. Luận án giải quyết khoảng trống này bằng cách đề xuất phương pháp sinh giả định yếu nhất cục bộ để tái sử dụng tối đa, giảm thiểu số lần phải sinh lại giả định.
  • Trong mô hình ERA có ràng buộc thời gian: Phương pháp hai pha của Lin và cộng sự có độ phức tạp cao. Luận án tập trung nghiên cứu, cài đặt thử nghiệm phiên bản một pha (loại bỏ pha không thời gian) và giải quyết các bài toán kỹ thuật phát sinh khi Teacher gặp trạng thái bế tắc hoặc lặp vô hạn.

Cơ sở lý thuyết và phương pháp nghiên cứu

Luận án sử dụng các khung lý thuyết hình thức, định nghĩa toán học và phương pháp thực nghiệm kỹ thuật phần mềm:

  1. Khung lý thuyết và mô hình đặc tả:
  • Hệ chuyển trạng thái được gán nhãn (LTS): Mô hình hóa bằng bộ bốn $M = \langle Q, \Sigma, \delta, q_0 \rangle$, kích thước $|M| = |Q|$, chuỗi hành vi $\sigma$, ngôn ngữ $L(M)$, phép ghép nối song song $M_1 \parallel M_2$, thuộc tính an toàn $p$, LTS lỗi $p_{err} = \langle Q \cup {\pi}, \Sigma_p, \delta', q_0 \rangle$, và ô-tô-mát hữu hạn trạng thái đơn định DFA $D = \langle Q, \Sigma, \delta, q_0, F \rangle$.
  • Khái niệm tiến hóa phần mềm: Phần mềm $M$ tiến hóa thành $M'$ khi $L(M) \neq L(M')$ và $L(M) \cap L(M') \neq \emptyset$.
  • Các khái niệm giả định: Giả định mạnh nhất cục bộ $A_{LS}$ thỏa mãn $\forall A \in \mathcal{A}: L(A_{LS})\uparrow_{\Sigma_A} \subseteq L(A)$; Giả định nhỏ nhất cục bộ $A_{LM}$ thỏa mãn $\forall A \in \mathcal{A}: |A_{LM}| \le |A|$; Giả định yếu nhất cục bộ $A_{LW}$ thỏa mãn $\forall A \in \mathcal{A}: L(A) \subseteq L(A_{LW})$.
  • Hệ thống chuyển trạng thái bằng lôgic mệnh đề: Bộ ba $M = \langle X, \iota(X), \tau(X, X') \rangle$ trên miền $\mathbb{B} = {T, F}$, phép gán $v$, phép chiếu $v|_Y$, quan hệ mô phỏng $M \preceq N$ ($L(M) \subseteq L(N)$), phép ghép nối $M_1 \parallel M_2 = \langle X_1 \cup X_2, \iota_1 \wedge \iota_2, \tau_1 \wedge \tau_2 \rangle$.
  • Hệ thống có ràng buộc thời gian (ERA): Ô-tô-mát ghi sự kiện $M = (\Sigma, L, L_0, \delta, L_f)$, tập đồng hồ $C_\Sigma = {x_a \mid a \in \Sigma}$, từ có thời gian $w_t$, từ đồng hồ $w_c$, gác đồng hồ $g \in G_\Sigma$, từ gác $w_g$, và hàm hậu điều kiện mạnh nhất $sp(\varphi, w_g)$.
  1. Mô hình kiểm chứng tương tác Learner - Teacher: Kiểm chứng giả định - đảm bảo vận hành thông qua hai thực thể:
  • Learner: Thực thi thuật toán học ngôn ngữ/hàm lôgic ($L^$, CDNF, $TL^$) để sinh các ứng viên giả định $A$.
  • Teacher: Trả lời hai loại câu hỏi từ Learner: Truy vấn thành viên ($Q_m$) để xác định chuỗi $\sigma$ có thuộc ngôn ngữ giả định $L(A)$ hay không; và Truy vấn ứng viên ($Q_{eq}$) để kiểm tra $A$ có thỏa mãn luật kiểm chứng giả định - đảm bảo hay không (trả về kết quả ${YES, NO + cex, UNSAT + cex}$).
Thành phần nghiên cứu Mô hình đặc tả LTS Mô hình Lôgic mệnh đề Mô hình Ô-tô-mát ghi sự kiện (ERA)
Thuật toán học cơ sở Thuật toán $L^*$ (Angluin, Rivest) Thuật toán CDNF (Bshouty) Thuật toán $TL^*$ (Lin và cs)
Cấu trúc dữ liệu trung gian Bảng quan sát $(S, E, T)$ Bảng chân lý / Phép gán lôgic Bảng quan sát thời gian / Từ gác
Quy tắc kiểm chứng (NC-AG) $\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}$ $\frac{M_1 \parallel A \models p \quad M_2 \preceq A}{M_1 \parallel M_2 \models p}$ $\frac{M_1 \models_A p \quad M_2 \models A}{M_1 \parallel M_2 \models p}$
Mục tiêu cải tiến Sinh giả định $A_{LM}$ và $A_{LS}$ Sinh giả định $A_{LW}$ cho kiểm chứng hồi quy Cài đặt phiên bản một pha
Công cụ cài đặt thực nghiệm LMAG, LSAG LWAG, CBAG Tivet
  1. Phương pháp nghiên cứu thực nghiệm: Luận án kết hợp giữa chứng minh hình thức (chứng minh tính đúng đắn và tính đầy đủ của các thuật toán đề xuất) và kiểm nghiệm thực nghiệm trên các hệ thống benchmark phổ biến trong cộng đồng nghiên cứu như: Hệ thống sản xuất linh hoạt (Flexible Manufacturing System - FMS), Hệ thống trạm cung cấp nhiên liệu (Gas Station System - GSS). Các chỉ số định lượng được đo lường bao gồm: số lượng trạng thái của giả định, không gian trạng thái giảm được, số lượng câu truy vấn thành viên/ứng viên, số lần sinh lại giả định, và thời gian thực thi (tính bằng giây).

Nội dung chính theo từng chương

Chương 1. Giới thiệu

Chương này phân tích bối cảnh phát triển phần mềm theo hướng module hóa và thành phần (CBSE), đặt ra yêu cầu kiểm chứng các thuộc tính an toàn của hệ thống. Tác giả phân tích hạn chế của phương pháp kiểm chứng mô hình vét cạn do bùng nổ không gian trạng thái, từ đó giới thiệu phương pháp kiểm chứng giả định - đảm bảo (AGV). Chương 1 trình bày sơ đồ tổng quan về AGV, xác định rõ 3 vấn đề còn tồn tại tương ứng với 3 loại đặc tả (LTS, lôgic mệnh đề, ERA), phát biểu 3 mục tiêu nghiên cứu, nêu tóm tắt 3 đóng góp chính và trình bày bố cục 6 chương của luận án.

Chương 2. Kiến thức nền tảng

Chương 2 thiết lập hệ thống định nghĩa toán học làm cơ sở cho toàn bộ luận án:

  • Trình bày chi tiết cú pháp và ngữ nghĩa của LTS, tích song song, thuộc tính an toàn, LTS lỗi $p_{err}$, DFA và bảng quan sát $(S, E, T)$.
  • Trình bày mô hình hệ thống chuyển trạng thái đặc tả bằng lôgic mệnh đề, hàm khởi tạo $\iota(X)$, hàm chuyển trạng thái $\tau(X, X')$, quan hệ mô phỏng $M \preceq N$, và phép ghép nối các thành phần.
  • Trình bày hệ thống có ràng buộc thời gian với ô-tô-mát ghi sự kiện ERA, đồng hồ ghi sự kiện $C_\Sigma$, từ có thời gian, từ gác và hàm hậu điều kiện $sp(\varphi, w_g)$.
  • Thiết lập luật kiểm chứng giả định - đảm bảo không quay vòng (NC-AG) cho từng loại đặc tả; định nghĩa hình thức các khái niệm giả định yếu nhất ($A_W$), giả định mạnh nhất ($A_S$), giả định nhỏ nhất ($A_M$), giả định mạnh nhất cục bộ ($A_{LS}$), giả định nhỏ nhất cục bộ ($A_{LM}$) và giả định yếu nhất cục bộ ($A_{LW}$).
  • Trình bày mô hình tương tác Learner - Teacher, phân loại câu truy vấn thành viên $Q_m$ và truy vấn ứng viên $Q_{eq}$.

Chương 3. Phương pháp sinh giả định nhỏ nhất và mạnh nhất cục bộ cho việc kiểm chứng phần mềm dựa trên thành phần

Chương này tập trung vào bài toán kiểm chứng phần mềm đặc tả bằng LTS:

  • Phân tích hạn chế của thuật toán sinh giả định dựa trên $L^*$ của Cobleigh và cộng sự (Thuật toán 3.1): việc trả về true cho mọi chuỗi $s \in L(A_W)$ dẫn đến việc giả định sinh ra có ngôn ngữ lớn hơn mức cần thiết.
  • Đưa ra phản ví dụ cụ thể (Hình 3.3) chứng minh tồn tại giả định $A_{LS}$ mạnh hơn giả định $A$ sinh bởi thuật toán của Cobleigh, được kiểm chứng đối chứng bằng công cụ LTSA ($A_{LS} \models A$).
  • Đề xuất biến thể thuật toán trả lời truy vấn thành viên (Thuật toán 3.2): Khi chuỗi $s \in L(A_W)$, Teacher trả về giá trị "?" thay vì true. Learner tạm thời coi "?" là false để sinh giả định có ngôn ngữ nhỏ hơn (mạnh hơn); nếu không tìm được giả định thỏa mãn mới quay lui coi là true.
  • Đề xuất thuật toán sinh giả định nhỏ nhất và mạnh nhất cục bộ: Duyệt các ứng viên giả định $A_i$ với kích thước trạng thái tăng dần $t$ ($1 \le t \le |A_i|$). Trong các ứng viên cùng kích thước $t$, thuật toán kiểm tra các tập chuỗi từ $1$ đến $n-1$ chuỗi thuộc ngôn ngữ $L(C)$, dừng ngay khi tìm được giả định đầu tiên thỏa mãn luật kiểm chứng.
  • Chứng minh tính đúng đắn toán học của phương pháp đề xuất.
  • Xây dựng công cụ LMAG, LSAG và thực nghiệm trên các hệ thống benchmark, ghi nhận kết quả so sánh giữa Thuật toán 3.1 và phương pháp đề xuất về kích thước giả định, thời gian kiểm chứng và tỷ lệ không gian trạng thái giảm được.

Chương 4. Phương pháp kiểm chứng hồi quy giả định - đảm bảo cho phần mềm tiến hóa

Chương này nghiên cứu phương pháp kiểm chứng cho phần mềm đặc tả bằng lôgic mệnh đề:

  • Phân tích thuật toán CDNF và phương pháp CBAG của Chen và cộng sự, He và cộng sự, chỉ ra hạn chế phải sinh lại giả định trong mọi trường hợp phần mềm tiến hóa.
  • Đề xuất thuật toán LWAG (Local Weakest Assumption Generation) sinh giả định yếu nhất cục bộ ($A_{LW}$) thông qua biến thể thuật toán trả lời truy vấn thành viên và thuật toán quay lui.
  • Xây dựng quy trình kiểm chứng hồi quy giả định - đảm bảo từng phần: Khi phần mềm tiến hóa từ $M$ sang $M'$, thuật toán tận dụng lại giả định $A_{LW}$ đã sinh trước đó. Quá trình kiểm chứng chỉ yêu cầu sinh lại giả định khi $A_{LW}$ không còn thỏa mãn các thành phần tiến hóa mới.
  • Chứng minh tính đúng đắn và tính đầy đủ của thuật toán đề xuất.
  • Thực nghiệm so sánh phương pháp đề xuất (LWAG) với phương pháp CBAG trên các ca kiểm thử: Bảng 4.2 và Bảng 4.3 ghi nhận quá trình sinh giả định ban đầu và sinh giả định trong ngữ cảnh tiến hóa; Bảng 4.4 và Bảng 4.5 so sánh tổng hợp số lần sinh lại giả định và thời gian thực thi, chứng minh hiệu quả giảm số lần sinh lại giả định khi phần mềm tiến hóa.

Chương 5. Thử nghiệm cài đặt phiên bản một pha cho việc kiểm chứng giả định - đảm bảo cho phần mềm có ràng buộc thời gian

Chương này nghiên cứu bài toán kiểm chứng cho hệ thống có ràng buộc thời gian đặc tả bằng ERA:

  • Phân tích phương pháp kiểm chứng hai pha của Lin và cộng sự (Pha 1: sinh giả định không có thời gian; Pha 2: sinh giả định có thời gian dựa trên $TL^*$).
  • Đề xuất và cài đặt phiên bản một pha: Loại bỏ hoàn toàn pha thứ nhất, trực tiếp sinh giả định có ràng buộc thời gian nhằm tinh giản quy trình.
  • Phát hiện và đưa ra giải pháp kỹ thuật cho các vấn đề phát sinh trong cài đặt thực tế:
    1. Xử lý trường hợp Teacher "không biết" (không xác định được khả năng tiếp tục sinh giả định hoặc không xác định được phản ví dụ trả về cho Learner).
    2. Hiện thực hóa cơ chế tạo và phân tích phản ví dụ ($cex$) giữa Teacher và Learner để tinh chỉnh ứng viên giả định.
    3. Xử lý trường hợp quá trình sinh giả định rơi vào vòng lặp vô hạn.
  • Chứng minh tính đúng đắn của phiên bản một pha.
  • Cài đặt công cụ Tivet và thực nghiệm trên các hệ thống có ràng buộc thời gian mẫu, ghi nhận kết quả tại Bảng 5.2 về tính khả thi và thời gian kiểm chứng.

Chương 6. Kết luận và hướng phát triển tiếp theo

Chương này tổng kết toàn bộ các kết quả đạt được của luận án và đề xuất các hướng nghiên cứu tiếp theo nhằm hoàn thiện phương pháp kiểm chứng hình thức.

Kết quả và những đóng góp mới

Luận án đạt được các đóng góp về mặt lý luận và thực tiễn như sau:

  1. Về mặt lý thuyết và phương pháp:
  • Đề xuất phương pháp sinh giả định nhỏ nhất và mạnh nhất cục bộ cho bài toán kiểm chứng giả định - đảm bảo trên mô hình LTS, dựa trên biến thể truy vấn thành viên trả về giá trị "?" và chiến lược duyệt không gian ứng viên tăng dần theo kích thước và tập chuỗi. Chứng minh tính đúng đắn hình thức của thuật toán.
  • Đề xuất phương pháp sinh giả định yếu nhất cục bộ ($A_{LW}$) và quy trình kiểm chứng hồi quy cho phần mềm đặc tả bằng lôgic mệnh đề trong ngữ cảnh tiến hóa, giúp giảm tối đa số lần phải sinh lại giả định khi các thành phần thay đổi.
  • Đề xuất và chứng minh tính đúng đắn của phiên bản kiểm chứng một pha trên mô hình ô-tô-mát ghi sự kiện (ERA), loại bỏ pha không thời gian trong phương pháp hai pha của Lin và cộng sự; đồng thời đưa ra giải pháp xử lý các trạng thái bế tắc kỹ thuật ("Teacher không biết") và hiện tượng lặp vô hạn.
  1. Về mặt thực tiễn và công cụ phần mềm:
  • Thiết kế, cài đặt và tích hợp các bộ công cụ phần mềm hỗ trợ kiểm chứng tự động: công cụ LMAG/LSAG (cho mô hình LTS), LWAG (cho mô hình lôgic mệnh đề), và Tivet (cho mô hình ERA có ràng buộc thời gian).
  • Thực nghiệm kiểm chứng trên các hệ thống benchmark phổ biến (FMS, GSS), cung cấp các số liệu thực nghiệm định lượng minh chứng cho khả năng giảm kích thước không gian trạng thái, giảm thời gian tính toán và giảm số lần sinh lại giả định.
  1. Kiến nghị áp dụng trong kỹ nghệ phần mềm:
  • Đối với các phần mềm được mô hình hóa ở mức trừu tượng cao (mức thiết kế kiến trúc) dưới dạng hệ chuyển trạng thái, khuyến nghị áp dụng phương pháp sinh giả định nhỏ nhất và mạnh nhất cục bộ (Chương 3) để tối ưu không gian trạng thái.
  • Đối với các quy trình kiểm chứng yêu cầu tốc độ xử lý nhanh, kiểm chứng hồi quy liên tục và hệ thống được mô hình hóa ở mức thấp dưới dạng lôgic mệnh đề, khuyến nghị áp dụng phương pháp kiểm chứng dựa trên giả định yếu nhất cục bộ LWAG (Chương 4).
  • Đối với các hệ thống thời gian thực có yêu cầu đồng hồ sự kiện nghiêm ngặt, khuyến nghị đặc tả bằng ERA và áp dụng phương pháp kiểm chứng một pha (Chương 5).

Hạn chế và hướng nghiên cứu tiếp

Hạn chế của luận án:

  • Luận án mới chỉ tập trung vào việc kiểm chứng thuộc tính an toàn (safety properties), chưa mở rộng kiểm chứng cho thuộc tính sống (liveness properties) trên toàn bộ các mô hình.
  • Do độ phức tạp tính toán của bài toán kiểm chứng toàn cục, các giả định tối ưu sinh ra trong Chương 3 và Chương 4 mới đạt mức tối ưu cục bộ trong không gian tìm kiếm khả thi của thuật toán đề xuất, chưa thể bao quát toàn bộ tập giả định toàn cục.
  • Phiên bản cài đặt một pha trên mô hình ERA trong Chương 5 vẫn phát sinh các trường hợp lặp vô hạn hoặc bế tắc cần sự can thiệp của các quy tắc xử lý biên.

Hướng nghiên cứu tiếp theo:

  • Mở rộng các thuật toán sinh giả định để hỗ trợ kiểm chứng các thuộc tính sống (liveness properties) và các thuộc tính thời gian phức tạp hơn.
  • Nghiên cứu cải tiến thuật toán Teacher và cơ chế phân tích phản ví dụ cho ô-tô-mát ghi sự kiện nhằm loại bỏ hoàn toàn các trường hợp bế tắc và lặp vô hạn.
  • Mở rộng phạm vi thử nghiệm thực nghiệm trên các hệ thống phần mềm công nghiệp quy mô lớn và tích hợp công cụ vào các môi trường phát triển phần mềm tự động (CI/CD).

Giá trị tham khảo

Luận án cung cấp tài liệu tham khảo cho các đối tượng và mục đích sử dụng sau:

  • Nghiên cứu sinh và học viên cao học chuyên ngành Kỹ thuật phần mềm, Khoa học máy tính: Tham khảo phương pháp luận nghiên cứu hình thức (Formal Methods), cách thức tiếp cận và cải tiến các thuật toán học máy ngôn ngữ ($L^$, CDNF, $TL^$) kết hợp với kiểm chứng mô hình (Model Checking).
  • Giảng viên và nhà nghiên cứu: Sử dụng làm tài liệu chuyên đề giảng dạy về Kiểm thử và kiểm chứng phần mềm, Phương pháp hình thức trong phát triển phần mềm, và Kỹ thuật phần mềm dựa trên thành phần.
  • Kỹ sư phát triển phần mềm và chuyên gia đảm bảo chất lượng hệ thống nhúng/hệ thống thời gian thực: Tham khảo các thuật toán trong Chương 3, Chương 4 và Chương 5 cùng mã nguồn/nguyên lý cài đặt của các công cụ LMAG, LWAG, Tivet để áp dụng kiểm chứng tự động các thành phần phần mềm quan trọng trong công nghiệp ô tô, viễn thông và điều khiển tự động.

Câu hỏi thường gặp

  1. Tại sao phương pháp sinh giả định dựa trên thuật toán $L^$ của Cobleigh và cộng sự không sinh được giả định mạnh nhất?*
    Phương pháp của Cobleigh và cộng sự dựa vào ngôn ngữ của giả định yếu nhất $L(A_W)$ để trả lời các câu truy vấn thành viên. Khi một chuỗi $s \in L(A_W)$, thuật toán luôn trả về kết quả true, khiến cho ngôn ngữ của giả định sinh ra bị mở rộng bằng với ngôn ngữ của giả định yếu nhất. Hơn nữa, thuật toán dừng ngay khi tìm được kết quả kiểm chứng đầu tiên mà không tiếp tục tối ưu hóa ngôn ngữ, dẫn đến giả định sinh ra không đạt được tính chất mạnh nhất (ngôn ngữ nhỏ nhất có thể).

  2. Biến thể của kỹ thuật trả lời truy vấn thành viên trong Chương 3 hoạt động như thế nào để hỗ trợ sinh giả định mạnh nhất cục bộ?
    Trong Thuật toán 3.2, khi Teacher kiểm tra thấy chuỗi $s \in L(A_W)$ (thỏa mãn $\langle [s] \rangle M_1 \langle p \rangle$), thay vì trả về true, Teacher sẽ trả về giá trị "?". Khi nhận được "?", Learner sẽ tạm thời xử lý giá trị này như false (loại chuỗi $s$ ra khỏi ngôn ngữ của giả định) để cố gắng sinh một giả định mạnh hơn có kích thước ngôn ngữ nhỏ hơn. Nếu không tìm được giả định thỏa mãn luật kiểm chứng, Learner mới quay lui lại và gán giá trị "?" thành true.

  3. Lợi ích của việc sử dụng giả định yếu nhất cục bộ ($A_{LW}$) trong kiểm chứng hồi quy phần mềm tiến hóa ở Chương 4 là gì?
    Giả định yếu nhất cục bộ ($A_{LW}$) là giả định có ngôn ngữ bao phủ tối đa các hành vi hợp lệ của môi trường cục bộ. Khi phần mềm tiến hóa từ $M$ thành $M'$ (thay đổi một số hành vi của thành phần), việc sử dụng $A_{LW}$ giúp tăng xác suất để các thành phần mới đã tiến hóa vẫn mô phỏng được giả định cũ ($M'2 \preceq A{LW}$). Nhờ đó, hệ thống không cần phải kích hoạt lại quá trình học để sinh lại giả định, giảm thiểu số lần sinh lại giả định và tiết kiệm thời gian kiểm chứng hồi quy.

  4. Những vấn đề phát sinh trong thực tế khi cài đặt phiên bản kiểm chứng một pha cho ERA ở Chương 5 và cách tác giả xử lý là gì?
    Khi loại bỏ pha không thời gian để cài đặt phiên bản một pha, luận án chỉ ra ba vấn đề phát sinh: (i) Teacher rơi vào trạng thái "không biết" (không xác định được tính hợp lệ của ứng viên hoặc phản ví dụ cần trả về); (ii) Learner gặp khó khăn trong việc phân tích phản ví dụ thời gian để tinh chỉnh ứng viên; và (iii) Quá trình sinh ứng viên rơi vào vòng lặp vô hạn. Tác giả đã xử lý bằng cách hiện thực hóa thuật toán phân tích phản ví dụ chi tiết cho Teacher/Learner, bổ sung các điều kiện dừng và cơ chế xử lý ngoại lệ khi Teacher gặp trạng thái chưa xác định.

  5. Luận án đã cài đặt và sử dụng những công cụ phần mềm nào để phục vụ thực nghiệm?
    Luận án đã cài đặt và sử dụng các công cụ: LMAG và LSAG (công cụ sinh giả định nhỏ nhất và mạnh nhất cục bộ trên mô hình LTS); CBAG và LWAG (công cụ sinh giả định dựa trên CDNF và sinh giả định yếu nhất cục bộ trên mô hình lôgic mệnh đề); Tivet (công cụ kiểm chứng hệ thống có ràng buộc thời gian trên mô hình ERA); đồng thời sử dụng công cụ LTSA và PAT làm đối chứng kiểm chứng hình thức.

Kết luận

Luận án đã giải quyết bài toán tối ưu hóa chi phí thời gian trong kiểm chứng giả định - đảm bảo cho phần mềm dựa trên thành phần trên ba mô hình đặc tả hình thức gồm LTS, lôgic mệnh đề và ô-tô-mát ghi sự kiện (ERA). Các đóng góp chính bao gồm phương pháp sinh giả định nhỏ nhất và mạnh nhất cục bộ trên LTS, phương pháp sinh giả định yếu nhất cục bộ phục vụ kiểm chứng hồi quy trong ngữ cảnh tiến hóa trên mô hình lôgic mệnh đề, và thử nghiệm cài đặt thành công phiên bản kiểm chứng một pha cho hệ thống có ràng buộc thời gian trên ERA. Các thuật toán đề xuất đều được chứng minh tính đúng đắn toán học và được kiểm nghiệm thông qua việc phát triển các công cụ hỗ trợ thực nghiệm (LMAG, LSAG, LWAG, Tivet), mang lại cơ sở khoa học và giải pháp kỹ thuật hữu ích nhằm nâng cao hiệu quả kiểm chứng tự động chất lượng phần mềm.