Tổng quan luận án

Phát triển phần mềm thời gian thực dựa trên thành phần (Component-Based Real-Time Software Development - CB-RTS) là một hướng tiếp cận quan trọng trong kỹ nghệ phần mềm hiện đại. Phương pháp này cho phép xây dựng các hệ thống phức tạp thông qua việc ghép nối dần các thành phần phần mềm độc lập cho đến khi thỏa mãn toàn bộ yêu cầu của hệ thống, giúp rút ngắn thời gian phát triển, tăng khả năng tái sử dụng và đơn giản hóa quy trình bảo trì. Tuy nhiên, thách thức kỹ thuật lớn nhất của cách tiếp cận này là việc đảm bảo tính đúng đắn của hệ thống sau khi tích hợp. Đặc biệt, trong các lĩnh vực yêu cầu độ tin cậy và an toàn nghiêm ngặt như hàng không vũ trụ, tự động hóa công nghiệp và an ninh quốc phòng, các lỗi thiết kế có thể dẫn đến thiệt hại nghiêm trọng. Phần lớn các lý thuyết và kỹ thuật phát triển dựa trên thành phần truyền thống chỉ tiến hành kiểm tra phần mềm ở giai đoạn triển khai hoặc thử nghiệm, trong khi yêu cầu thực tế đòi hỏi tính đúng đắn phải được chứng minh và kiểm soát ngay từ giai đoạn thiết kế kiến trúc.

Khoảng trống nghiên cứu then chốt mà luận án chỉ ra xuất phát từ hai phương pháp kiểm chứng hình thức phổ biến hiện nay:

  • Kiểm chứng mô hình (Model Checking): Thường sử dụng ôtômát thời gian để mô hình hóa hành vi hệ thống và kiểm tra các tính chất đặc tả bằng lôgíc thời gian (như LTL, CTL, MTL, MITL). Khi áp dụng vào các hệ thống quy mô lớn có sự kết hợp của nhiều thành phần, phương pháp này gặp phải hiện tượng bùng nổ không gian trạng thái (state space explosion), dẫn đến độ phức tạp tính toán rất cao. Thêm vào đó, việc tích hợp đồng thời các ràng buộc thời gian thực và các ràng buộc phi chức năng về tài nguyên (như hiệu năng CPU, dung lượng bộ nhớ, băng thông mạng, mức tiêu thụ năng lượng) càng làm gia tăng độ phức tạp kiểm chứng.
  • Chứng minh định lý (Theorem Proving): Dựa trên các phép suy diễn toán học hình thức, tuy nhiên phương pháp này phần lớn chỉ mới tập trung giải quyết các bài toán cho hệ thống phi thời gian và rất khó tự động hóa hoàn toàn.

Mục tiêu tổng quát của luận án là đề xuất các phương pháp, kỹ thuật đặc tả và kiểm chứng hình thức hiệu quả cho hệ thống thời gian thực dựa trên thành phần ngay từ giai đoạn thiết kế sớm, kết hợp chiến lược chia để trị với các nguyên lý tính đúng đắn bởi cách xây dựng (Correctness by Construction) và thiết kế bằng hợp đồng (Design by Contract).

Các nhiệm vụ và câu hỏi nghiên cứu cụ thể của luận án bao gồm:

  1. Xây dựng mô hình thành phần phần mềm thời gian thực có cấu trúc phân tách rõ ràng nhằm kiểm soát tương tranh và tối ưu hóa tài nguyên theo chiến lược chia để trị.
  2. Thiết lập thể thức tương tác tương tranh thời gian và thể thức tương tác ràng buộc tài nguyên, đồng thời xây dựng thuật toán kiểm chứng sự tuân thủ (compliance) của chuỗi hành vi môi trường đối với thành phần phần mềm.
  3. Mở rộng lý thuyết giao diện thành phần thành lý thuyết giao diện thời gian thực với quan hệ vào/ra, biểu diễn hữu hạn không gian hành vi bằng ôtômát khoảng và chứng minh tính cắm được (plugability).
  4. Xây dựng kỹ thuật đặc tả bằng hợp đồng thời gian và hợp đồng thời gian - tài nguyên chi tiết đến mức phương thức, đề xuất thuật toán ước lượng tài nguyên tiêu thụ và thiết lập ngôn ngữ đặc tả thời gian thực mẫu dựa trên Lý thuyết hợp nhất ngôn ngữ lập trình (UTP).

Đối tượng nghiên cứu của luận án là các phương pháp phát triển hệ thống thời gian thực dựa trên thành phần và cấu trúc hình thức của hệ thống thời gian thực dựa trên thành phần, xét trên cả hai phương diện: hệ thống cơ sở lý thuyết và kỹ thuật phần mềm thực tế. Phạm vi nghiên cứu tập trung vào các hệ thống thời gian thực (gồm thời gian thực nghiêm ngặt, ổn định và linh động) có ràng buộc tài nguyên, ứng dụng các công cụ mô hình hóa hình thức như ôtômát thời gian, ôtômát trọng số, ôtômát khoảng và các hệ lôgíc thời gian liên quan.

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

Trong quá trình xây dựng cơ sở khoa học, luận án đã tổng quan các công trình nghiên cứu nền tảng trong nước và quốc tế thuộc các nhóm hướng nghiên cứu chính:

  • Lý thuyết và định nghĩa về thành phần phần mềm: Clemens Szyperski (1998, 2002) định nghĩa thành phần phần mềm là đơn vị hợp thành với giao diện đặc tả theo hợp đồng và phụ thuộc ngữ cảnh rõ ràng; Bertrand Meyer (1997, 2003) nhấn mạnh tính mô-đun được đặc tả hình thức và phục vụ các bên sử dụng độc lập; George T. Heineman và William T. Councill (2001) gắn thành phần với sự tuân thủ một mô hình thành phần cụ thể.
  • Nguyên lý tính đúng đắn bởi cách xây dựng: Các nghiên cứu của Anthony Hall và Roderick Chapman (2002), Gregor Gössler và Joseph Sifakis (2003, 2005), Đặng Văn Hưng và đồng nghiệp, Derrick G. Kourie và Bruce W. Watson (2012) xác lập các tiêu chí về xây dựng thành phần nguyên tử đúng đắn, luật phối ghép bảo toàn tính chất, và cơ chế thiết lập tiền điều kiện, hậu điều kiện cùng các bất biến.
  • Các mô hình thành phần và kiến trúc phần mềm: Các công nghệ thành phần hướng đối tượng công nghiệp (CORBA, EJB, COM, DCOM); mô hình PECOS (PErvasive COmponent Systems) phát triển cho hệ thống nhúng giới hạn tài nguyên; mô hình BIP (Behaviour-Interaction-Priority) với kiến trúc 3 tầng phân định hành vi, giao thức tương tác và ưu tiên giải quyết xung đột; mô hình X-MAN (Nannan He, K. Lau) trong dự án CESAR hỗ trợ ghép nối bằng bộ kết nối và điều phối; lý thuyết rCOS hỗ trợ tinh giảm tính toán cho hệ thống đối tượng; ngôn ngữ kịch bản của Nicola Nostro và đồng nghiệp.
  • Mô hình hóa và kiểm chứng hệ thống thời gian thực: Lý thuyết ôtômát thời gian (Timed Automata) và ôtômát vùng (Region Automata) của Rajeev Alur và David L. Dill (1994); ôtômát trọng số (Priced Timed Automata) của Behrmann, Larsen và cộng sự; tính toán khoảng (Duration Calculus) của Chu S. Zhou, C.A.R. Hoare, Anders P. Ravn và ôtômát khoảng (Duration Automata) của Đặng Văn Hưng; các công cụ kiểm chứng mô hình thời gian thực (UPPAAL, UPPAAL-SMC, Kronos, HyTech, PRISM, MRMC, ECDAR, TIMES); các hệ lôgíc thời gian (LTL của Pnueli, CTL của Clarke và Emerson, MTL của Koymans, MITL của Alur, Feder và Henzinger); Lý thuyết hợp nhất ngôn ngữ lập trình (UTP) của C.A.R. Hoare và He Jifeng; lý thuyết đại số giao diện (Interface Algebra) của Luca de Alfaro và Thomas A. Henzinger.
Tiêu chí so sánh COM / DCOM / CORBA Mô hình PECOS Mô hình BIP Mô hình X-MAN Mô hình đề xuất của luận án
Hỗ trợ thời gian thực Không hỗ trợ Rất hạn chế Không hỗ trợ trực tiếp Không hỗ trợ Hỗ trợ đầy đủ qua $\omega$-automata, TA, DA
Ràng buộc tài nguyên Không xét đến Hỗ trợ tĩnh cho nhúng Không hỗ trợ Không hỗ trợ Ôtômát trọng số (PTA) và biểu thức $\eth$
Hỗ trợ tương tranh Đa luồng cơ bản Chưa hỗ trợ đa luồng Xử lý qua tầng tương tác Bộ điều phối kết nối Biểu thức chính quy trên bảng chữ cái phân tán
Thiết kế bằng hợp đồng Giao diện chữ ký hàm Không áp dụng Không áp dụng Hợp đồng tiền/hậu điều kiện Hợp đồng thời gian và thời gian - tài nguyên
Thành phần bất biến Không có Không có Không có Không có Bất biến chức năng và bất biến tài nguyên
Kiến trúc thành phần Đơn tầng Mô-đun nhúng 3 tầng (Thành phần/Giao thức/Ưu tiên) Nguyên tử và Hợp thành Phân tách 2 phần: Chủ động và Thụ động

Khoảng trống nghiên cứu được luận án lựa chọn giải quyết là sự thiếu vắng một khung phương pháp luận hình thức hoàn chỉnh cho phép: (1) mô hình hóa cấu trúc thành phần thời gian thực phân định rõ vai trò chủ động tương tác và thụ động cung cấp dịch vụ; (2) đặc tả chính xác thể thức tương tác tương tranh kết hợp ràng buộc tài nguyên phi chức năng; (3) mô hình hóa giao diện thời gian thực bằng ôtômát khoảng để giải quyết tính vô hạn của chuỗi hành vi; và (4) xây dựng hệ thống ngôn ngữ đặc tả mẫu thống nhất dựa trên hợp đồng thời gian - tài nguyên.

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

Luận án sử dụng hệ thống cơ sở lý thuyết toán học và kỹ nghệ phần mềm hình thức gồm các trụ cột sau:

Cơ sở lý thuyết

  • Phân loại hệ thống thời gian thực: Luận án phân định 4 nhóm hệ thống gồm hệ thống thời gian thực nghiêm ngặt (hard real-time, kết quả sai mốc thời gian xem như hỏng toàn bộ hệ thống), ổn định (firm real-time, kết quả trễ hạn mất giá trị sử dụng nhưng không làm dừng hệ thống), linh động (soft real-time, kết quả trễ hạn làm suy giảm chất lượng dịch vụ) và phi thời gian (non-real-time, ràng buộc thời gian bằng 0). Hệ thống phải thỏa mãn 3 tính chất cốt lõi: tính kịp thời, tính dự đoán và tính xử lý đồng thời.
  • Lý thuyết Ôtômát thời gian và Ôtômát vùng: Ôtômát thời gian $M = \langle L, \Sigma, l_0, \mathcal{C}, T, \Gamma \rangle$ hoạt động trên bảng chữ cái $\Sigma$ và tập đồng hồ $\mathcal{C}$, nhận dạng các từ thời gian $\omega = (\sigma, \tau) \in (\Sigma \times \mathbb{R}{\ge 0})^*$. Hệ thống có hai hình thức dịch chuyển: dịch chuyển thời gian trôi $\langle l, \nu \rangle \xrightarrow{d} \langle l, \nu + d \rangle$ và dịch chuyển rời rạc. Để biểu diễn không gian trạng thái vô hạn của tập đồng hồ thực $\mathbb{R}{\ge 0}$, luận án sử dụng ôtômát vùng $\mathcal{R}(M)$ dựa trên quan hệ tương đương vùng $\sim$ giữa các phép gán đồng hồ $\nu, \nu'$.
  • Lý thuyết Ôtômát trọng số (Priced Timed Automaton - PTA): Mở rộng ôtômát thời gian với cấu trúc $M = (L, l_0, \Sigma, T, H, \lambda, \Gamma)$, trong đó $H: L \to \Phi(\mathcal{C})$ là hàm gán bất biến lên vị trí và $\lambda: L \cup T \to \mathbb{N}$ là hàm gán chi phí tài nguyên lên vị trí và cạnh chuyển tiếp. Chi phí của một chuỗi thực thi $\rho$ được xác định bằng $\text{cost}(\rho) = \sum_{i=1}^n z_i$, cho phép xác định chi phí tối thiểu $\text{mincost}(\langle l_k, \nu_k \rangle)$ để hoàn thành chuỗi dịch vụ.
  • Tính toán khoảng và Ôtômát khoảng (Duration Automata): Sử dụng tập các khoảng thời gian tĩnh $\text{Time} = {[b, e] \mid b \in \mathbb{R}{\ge 0}, e \in \mathbb{R}{\ge 0} \cup {\infty} \wedge b \le e}$ gắn với từng dịch chuyển của giao diện. Các phép toán trên khoảng bao gồm phép giao khoảng $I_1 \cap I_2 = [\max(b_1, b_2), \min(e_1, e_2)]$, quan hệ khoảng con $I_1 \subseteq I_2$, và phép cộng nối tiếp khoảng $I_1 \cdot_\theta I_2 = [(b_1 + b_2), (b_1 + e_2)]$. Ôtômát khoảng được định nghĩa là bộ $M = \langle Q, \Sigma, q_0, T, \Gamma \rangle$ với tập chuyển tiếp $T \subseteq Q \times \Sigma \times \text{Time} \times Q$, biểu diễn hữu hạn các hành vi có chặn trên và chặn dưới thời gian.
  • Lý thuyết hợp nhất ngôn ngữ lập trình (UTP): Cung cấp nền tảng toán học dựa trên bảng chữ cái quan hệ, tiền điều kiện, hậu điều kiện và biểu thức lôgíc vị từ cấp 1 $\mathcal{F}(X \cup Y)$ để hợp nhất các đặc tả chức năng và phi chức năng.

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

Luận án áp dụng phương pháp nghiên cứu hình thức (Formal Methods) kết hợp kiểm chứng mô hình theo hướng phân rã thành phần:

  • Phương pháp mô hình hóa cấu trúc và hành vi: chia tách hệ thống thành phần chủ động/thụ động; mô tả tương tác bằng biểu thức chính quy trên bảng chữ cái phân tán $\Sigma_i$; mô tả giao diện bằng quan hệ đại số vào/ra $\Phi$.
  • Phương pháp kiểm chứng tính rỗng của ngôn ngữ: Để kiểm chứng mô hình $M$ với đặc tả tính chất $S$, luận án áp dụng bài toán kiểm tra $\mathcal{L}(M) \cap \neg \mathcal{L}(S) = \emptyset$.
  • Thuật toán hóa quy trình kiểm chứng: Thiết lập các thuật toán kiểm tra tính tuân thủ thể thức của môi trường, thuật toán kiểm chứng tính cắm được của giao diện, và thuật toán ước lượng định lượng mức tiêu thụ tài nguyên ngay tại pha thiết kế.

Nguồn dữ liệu và tư liệu phục vụ nghiên cứu bao gồm các chuẩn đặc tả hình thức quốc tế, các bộ công cụ kiểm chứng thực nghiệm (như UPPAAL, BIP, PECOS), và các ca nghiên cứu điển hình (hệ thống máy bán hàng tự động, hệ thống điều tiết không khí và kiểm soát nhiệt độ).

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

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

Chương 1 thiết lập nền tảng bài toán nghiên cứu. Tác giả phân tích tính cấp thiết của việc bảo đảm tính đúng đắn cho các hệ thống thời gian thực dựa trên thành phần (CB-RTS) trong các hệ thống đòi hỏi độ an toàn cao. Chương này chỉ ra các hạn chế căn bản của việc kiểm chứng ở pha triển khai và hiện tượng bùng nổ không gian trạng thái khi kiểm chứng mô hình truyền thống cho các hệ thống ghép nối có ràng buộc thời gian và tài nguyên. Từ đó, chương xác định rõ đối tượng nghiên cứu, phạm vi khoa học và tóm lược ba nhóm đóng góp chính của luận án cùng cấu trúc tổng thể 5 chương.

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

Chương 2 hệ thống hóa toàn bộ khung lý thuyết phục vụ các đóng góp chuyên sâu:

  • Kỹ nghệ phần mềm dựa trên thành phần (CBSE): Phân tích chi tiết các định nghĩa của Szyperski, Meyer, Heineman và Councill; làm rõ các khái niệm hộp đen, giao diện thành phần (tập biến vào $X$, tập biến ra $Y$), phép làm mịn (refinement), cơ chế hợp đồng, và các phép ghép song song, ghép nối tiếp có tính đến độ trễ đồng bộ (Delay).
  • Nguyên lý tính đúng đắn bởi cách xây dựng: Trình bày 6 tiêu chí cốt lõi gồm tính đúng đắn thành phần nguyên tử, luật phối ghép bảo toàn tính chất ($\Pi(C_1, \dots, C_k) \models P \wedge P'$), thiết lập tiền/hậu điều kiện, bộ lọc bảo vệ, kiểm tra tuân thủ thể thức và xây dựng kho thành phần.
  • Kiến trúc hệ thống CB-RTS: Minh họa mô hình kiến trúc 4 tầng gồm Phần cứng, Hệ điều hành, Bộ khung phát triển phần mềm (framework) và Môi trường.
  • Lý thuyết hệ thống thời gian thực và mô hình hóa hình thức: Trình bày định nghĩa chuỗi thời gian $\tau$, từ thời gian $\omega \in (\Sigma \times \mathbb{R}_{\ge 0})^*$, cấu trúc ôtômát thời gian $\mathcal{A}$, phép phân hoạch không gian đồng hồ thành ôtômát vùng $\mathcal{R}(M)$; cấu trúc ôtômát trọng số PTA với hàm chi phí $\lambda$; đại số khoảng và ôtômát khoảng DA.
  • Bài toán kiểm chứng: Trình bày các hệ lôgíc đặc tả tính chất (LTL, CTL, MTL, MITL, DC), khảo sát các công cụ kiểm chứng (UPPAAL, PRISM, MRMC, PSV) và quy trình kiểm chứng bằng kiểm tra tính rỗng ngôn ngữ $\mathcal{L}(M) \cap \neg \mathcal{L}(S) = \emptyset$.

Chương 3. Mô hình thành phần phần mềm thời gian thực và thể thức tương tác

Chương 3 trình bày đóng góp cốt lõi thứ nhất của luận án:

  • Đề xuất mô hình thành phần phần mềm thời gian thực mở rộng từ PECOS: Mô hình chia tách thành phần thành hai phần độc lập:
    • Phần thụ động (Passive Part): Đóng vai trò kho chứa các thành phần phần mềm thụ động (passive components), cung cấp đầy đủ các dịch vụ chức năng cho đến khi thỏa mãn toàn bộ yêu cầu thiết kế hệ thống.
    • Phần chủ động (Active Part): Gồm các thành phần phần mềm chủ động (active components) tương tác trực tiếp với môi trường, tiếp nhận các yêu cầu ngoại vi, điều phối gọi dịch vụ từ phần thụ động xử lý và trả kết quả về môi trường. Mô hình hỗ trợ kiểm soát và cho phép các tiến trình ở cả hai phần thực thi song song theo chiến lược chia để trị nhằm giảm thiểu độ phức tạp tích hợp.
  • Thể thức tương tác tương tranh ràng buộc thời gian ($\pi$): Đặc tả thứ tự gọi dịch vụ trong thành phần bằng biểu thức chính quy thời gian $E_i$ trên bảng chữ cái phân tán $\Sigma_i$ ($\Omega = \bigcup_{i=1}^k \Sigma_i$), kết hợp mô hình hóa chuỗi hành vi môi trường bằng ôtômát thời gian. Luận án đề xuất thuật toán kiểm chứng tính cắm được của môi trường vào thành phần.
  • Thể thức tương tác thời gian thực ràng buộc tài nguyên ($\eth$): Tích hợp tập tài nguyên $\mathcal{R}$, phép toán kết hợp $\otimes$, hàm gán chi phí $\lambda$ và ôtômát trọng số. Luận án xây dựng bảng toán tử tăng giảm tài nguyên (Bảng 3.2) và thuật toán kiểm tra sự tuân thủ thể thức của chuỗi hành vi môi trường trên cả phương diện chức năng lẫn phi chức năng, bảo đảm việc sử dụng tài nguyên được cấp phát đạt hiệu quả tối ưu.

Chương 4. Đặc tả và mô hình hóa giao diện thời gian thực

Chương 4 tập trung vào đóng góp cốt lõi thứ hai:

  • Mở rộng lý thuyết giao diện thời gian thực: Giao diện thành phần được mô hình hóa thành bộ ba $\langle X, Y, \Phi \rangle$, trong đó $X$ là tập biến đầu vào, $Y$ là tập biến đầu ra, và $\Phi$ là tập các công thức lôgíc vị từ cấp 1 $\mathcal{F}(X \cup Y)$ kèm ràng buộc thời gian trên tập $\text{Time}$. Ngữ nghĩa giao diện khẳng định: nếu môi trường cung cấp tập giá trị đầu vào thỏa mãn tiền điều kiện trong khoảng thời gian quy định, giao diện cam kết trả dữ liệu đầu ra thỏa mãn hậu điều kiện trong khoảng thời gian $[b, e]$ tương ứng.
  • Biểu diễn hữu hạn bằng Ôtômát khoảng (Duration Automata): Do tập hành vi của giao diện thời gian thực là vô hạn trên trục thời gian thực $\mathbb{R}_{\ge 0}$, luận án sử dụng ôtômát khoảng để biểu diễn hữu hạn các chuỗi hành vi của giao diện và môi trường thông qua việc gán nhãn khoảng thời gian $[\min, \max]$ cho từng bước chuyển.
  • Các phép toán và tính chất trên giao diện: Định nghĩa hình thức và chứng minh các tính chất đại số (giao hoán, kết hợp) của phép ghép song song và phép ghép nối tiếp giao diện; hình thức hóa quan hệ làm mịn (refinement) và làm mịn dùng chung giữa các giao diện thành phần; chứng minh tính chất cắm được (plugability) bảo đảm tính tương thích giữa môi trường và thành phần phần mềm.

Chương 5. Đặc tả và kiểm chứng bằng hợp đồng thời gian thực với ràng buộc tài nguyên

Chương 5 phát triển đóng góp cốt lõi thứ ba:

  • Đặc tả thành phần bằng hợp đồng thời gian và hợp đồng thời gian - tài nguyên: Dựa trên nguyên lý thiết kế bằng hợp đồng, mỗi thành phần được đặc tả chi tiết đến từng phương thức, bao gồm tiền điều kiện, hậu điều kiện, quan hệ biến vào/ra, thời gian thực thi lớn nhất/nhỏ nhất và chi phí tiêu thụ tài nguyên.
  • Đặc tả thành phần bất biến và bất biến tài nguyên: Thiết lập các biểu thức bất biến chức năng và bất biến tài nguyên (sử dụng phép kết hợp bất biến $\uplus$ và lôgíc thời gian tuyến tính) nhằm ràng buộc trạng thái an toàn trong suốt vòng đời của thành phần. Thể thức tương tác tương tranh có ràng buộc tài nguyên được nhúng trực tiếp vào hợp đồng, quy định môi trường chỉ được gọi dịch vụ khi cung cấp đủ tài nguyên và tuân thủ đúng trình tự.
  • Thuật toán ước lượng tài nguyên hệ thống: Đề xuất thuật toán phân tích sự tương tác giữa môi trường và các thành phần để ước lượng tổng mức tiêu thụ tài nguyên (CPU, bộ nhớ, năng lượng...) ngay từ giai đoạn thiết kế kiến trúc ban đầu.
  • Ngôn ngữ đặc tả thời gian thực mẫu: Xây dựng trên nền tảng Lý thuyết hợp nhất ngôn ngữ lập trình (UTP), cung cấp hệ thống văn phạm hình thức đầy đủ (17 cấu trúc văn phạm từ Hình 5.1 đến 5.17) bao gồm: định danh, số nguyên, thuộc tính, thành phần tài nguyên, tài nguyên hệ thống, khoảng thời gian, khẳng định, bất biến, bất biến tài nguyên, biểu thức đặc tả hệ thống, thành phần cơ bản, đặc tả phương thức, thành phần phần mềm chủ động/thụ động và toàn hệ thống.

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

Luận án đã đạt được các kết quả khoa học chính sau:

  1. Mở rộng mô hình PECOS cho hệ thống thời gian thực dựa trên thành phần: Xây dựng mô hình phân tách hai phần (chủ động và thụ động), cho phép thực thi song song và giảm độ phức tạp hệ thống theo chiến lược chia để trị. Đề xuất thể thức tương tác tương tranh thời gian thực $\pi$ và thể thức tương tác ràng buộc tài nguyên $\eth$ dựa trên biểu thức chính quy trên bảng chữ cái phân tán và ôtômát trọng số, cùng thuật toán kiểm tra tính tuân thủ của chuỗi hành vi môi trường.
  2. Phát triển lý thuyết giao diện thời gian thực với quan hệ vào/ra: Đề xuất phương pháp đặc tả giao diện thời gian thực bằng bộ ba $\langle X, Y, \Phi \rangle$ và kỹ thuật biểu diễn hữu hạn không gian hành vi vô hạn bằng ôtômát khoảng (Duration Automata). Chứng minh tính đúng đắn, tính giao hoán, kết hợp của các phép ghép song song, ghép nối tiếp, quan hệ làm mịn và thuật toán kiểm chứng tính chất cắm được.
  3. Đề xuất kỹ thuật đặc tả hợp đồng thời gian - tài nguyên và ngôn ngữ đặc tả mẫu: Thiết lập phương pháp đặc tả thành phần chi tiết đến mức phương thức, tích hợp các thành phần bất biến tài nguyên $\uplus$. Đề xuất thuật toán ước lượng tài nguyên tiêu thụ sớm trong quá trình thiết kế và xây dựng ngôn ngữ đặc tả thời gian thực mẫu dựa trên UTP với hệ thống văn phạm hình thức hoàn chỉnh nhằm hợp nhất các đặc tả chức năng và phi chức năng.

Các kiến nghị, giải pháp rút ra từ nghiên cứu:

  • Ứng dụng quy trình phát triển tăng dần dựa trên tính đúng đắn bởi cách xây dựng và thiết kế bằng hợp đồng nhằm phát hiện, cô lập và xử lý sai sót kỹ thuật ngay từ pha thiết kế kiến trúc, giảm thiểu chi phí sửa lỗi ở các giai đoạn sau.
  • Tích hợp việc đánh giá các chỉ số phi chức năng (thời gian thực thi, chi phí tài nguyên) song song với kiểm chứng chức năng để nâng cao chất lượng toàn diện của phần mềm thời gian thực.

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

Hạn chế của nghiên cứu:

  • Nghiên cứu chủ yếu tập trung vào việc xây dựng khung lý thuyết toán học, mô hình hình thức và các thuật toán kiểm chứng; chưa phát triển thành một bộ công cụ phần mềm tích hợp hoàn chỉnh (end-to-end framework) có giao diện đồ họa hỗ trợ tự động hóa toàn bộ quy trình biên dịch và kiểm chứng cho người dùng công nghiệp.
  • Phạm vi mô hình hóa chưa mở rộng sâu cho các hệ thống thời gian thực phân tán quy mô lớn có độ trễ truyền thông mạng ngẫu nhiên hoặc các hệ thống thời gian thực có yếu tố xác suất/thống kê (probabilistic real-time systems).

Hướng phát triển tiếp theo:

  • Xây dựng và cài đặt bộ công cụ phần mềm tự động hóa nhằm hỗ trợ phân tích, biên dịch ngôn ngữ đặc tả thời gian thực mẫu và thực thi các thuật toán kiểm chứng tính tuân thủ, tính cắm được đã đề xuất.
  • Mở rộng mô hình thành phần và thể thức tương tác thời gian thực cho các hệ thống phân tán phức tạp, tích hợp các bộ kiểm chứng mô hình hiện hành (như UPPAAL, PRISM) và kết nối với các môi trường phát triển tích hợp (IDE).

Giá trị tham khảo

Luận án là tài liệu tham khảo khoa học hữu ích cho các nhóm đối tượng sau:

  • Nghiên cứu sinh, học viên cao học và nhà nghiên cứu: Thuộc các chuyên ngành Kỹ thuật Phần mềm, Khoa học Máy tính, Hệ thống Nhúng và Phương pháp hình thức. Luận án cung cấp khung lý thuyết hoàn chỉnh về ứng dụng ôtômát thời gian, ôtômát trọng số và ôtômát khoảng trong kỹ nghệ thành phần.
  • Giảng viên đại học: Sử dụng làm tài liệu tham khảo chuyên sâu cho các môn học sau đại học về Kiểm chứng mô hình, Phương pháp hình thức trong công nghệ phần mềm, và Thiết kế hệ thống thời gian thực.
  • Kỹ sư kiến trúc phần mềm và chuyên gia phát triển hệ thống: Những người làm việc trong các lĩnh vực yêu cầu an toàn cao (hàng không, tự động hóa, điều khiển nhúng, thiết bị y tế), đặc biệt hữu ích khi tham khảo kỹ thuật thiết kế bằng hợp đồng thời gian - tài nguyên và quy trình kiểm soát chất lượng phần mềm từ pha thiết kế.

Các phần có giá trị tham khảo chuyên sâu nhất gồm:

  • Chương 2: Phần tổng quan toán học về ôtômát thời gian, ôtômát vùng và ôtômát khoảng.
  • Chương 3 & 4: Kiến trúc phân tách hai phần mở rộng từ PECOS và kỹ thuật mô hình hóa giao diện bằng ôtômát khoảng.
  • Chương 5: Hệ thống văn phạm hình thức của ngôn ngữ đặc tả thời gian thực mẫu dựa trên UTP.

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

1. Kiến trúc mô hình thành phần phần mềm thời gian thực do luận án đề xuất có cấu trúc như thế nào và có ưu điểm gì so với mô hình PECOS gốc?
Trả lời: Mô hình đề xuất mở rộng từ PECOS được chia tách thành hai phần: phần chủ động (active part) và phần thụ động (passive part). Phần chủ động tương tác với môi trường, nhận yêu cầu và điều phối gọi dịch vụ; phần thụ động đóng vai trò kho lưu trữ các thành phần phần mềm để lắp ghép đáp ứng yêu cầu hệ thống. Khác với PECOS gốc (chỉ hỗ trợ nhúng tĩnh, đơn luồng), mô hình của luận án hỗ trợ đa tiến trình thực thi song song ở cả hai phần theo chiến lược chia để trị, đồng thời tích hợp thể thức tương tác thời gian thực và kiểm soát ràng buộc tài nguyên.

2. Tại sao luận án sử dụng ôtômát khoảng (Duration Automata) thay vì ôtômát thời gian thuần túy để mô hình hóa giao diện thời gian thực?
Trả lời: Do các chuỗi hành vi của giao diện thời gian thực diễn ra liên tục và vô hạn trên miền thời gian số thực, việc sử dụng ôtômát thời gian với các biến đồng hồ có thể dẫn đến không gian trạng thái vô hạn phức tạp. Ôtômát khoảng cho phép biểu diễn hữu hạn các chuỗi hành vi này bằng cách trừu tượng hóa trực tiếp khoảng thời gian chuẩn bị và cung cấp dịch vụ thành các cận thời gian tĩnh $[b, e]$ trên mỗi bước chuyển tiếp, giúp đơn giản hóa việc tính toán các phép ghép song song, ghép nối tiếp và chứng minh tính cắm được.

3. Thể thức tương tác thời gian thực ràng buộc tài nguyên ($\eth$) được đặc tả và kiểm chứng bằng công cụ toán học nào?
Trả lời: Thể thức $\eth$ được đặc tả bằng biểu thức chính quy trên bảng chữ cái phân tán $\Sigma_i$ kết hợp với ôtômát trọng số (Priced Timed Automata - PTA) chứa hàm gán chi phí tài nguyên $\lambda$ và các toán tử tăng giảm tài nguyên. Luận án đề xuất thuật toán kiểm tra sự tuân thủ (compliance) để đối sánh chuỗi hành vi của môi trường với thể thức của thành phần, bảo đảm môi trường cấp phát đủ tài nguyên và gọi dịch vụ đúng trình tự quy định.

4. Ngôn ngữ đặc tả thời gian thực mẫu của luận án được xây dựng dựa trên nền tảng lý thuyết nào và giải quyết bài toán gì?
Trả lời: Ngôn ngữ được xây dựng dựa trên Lý thuyết hợp nhất ngôn ngữ lập trình (UTP - Unifying Theories of Programming) của Hoare và He Jifeng. Ngôn ngữ này cung cấp 17 cấu trúc văn phạm hình thức nhằm hợp nhất các đặc tả chức năng (phương thức, thuộc tính, quan hệ vào/ra) và phi chức năng (khoảng thời gian thực thi, bất biến tài nguyên) trên cùng một cú pháp toán học nhất quán.

5. Bài toán kiểm tra tính rỗng của ngôn ngữ ($L(M) \cap \neg L(S) = \emptyset$) được vận dụng như thế nào trong quy trình kiểm chứng của luận án?
Trả lời: Trong quy trình kiểm chứng mô hình, hệ thống được biểu diễn bằng mô hình $M$ với ngôn ngữ $L(M)$, còn tính chất thiết kế cần kiểm tra được đặc tả bằng $S$ với ngôn ngữ $L(S)$. Thay vì so sánh trực tiếp, phương pháp tìm ngôn ngữ bù $\neg L(S)$ và kiểm tra phần giao $L(M) \cap \neg L(S)$. Nếu giao này là tập rỗng ($\emptyset$), hệ thống thỏa mãn tính chất thiết kế $S$; nếu khác rỗng, hệ thống chứa lỗi và chuỗi vết trong phần giao được sử dụng để định vị và cô lập sai sót.

Kết luận

Luận án tiến sĩ của tác giả Nguyễn Trịnh Đông đã giải quyết một cách có hệ thống bài toán mô hình hóa và kiểm chứng hình thức cho các hệ thống thời gian thực dựa trên thành phần (CB-RTS). Thông qua việc kết hợp các nguyên lý tính đúng đắn bởi cách xây dựng và thiết kế bằng hợp đồng, công trình đã đề xuất ba nhóm đóng góp khoa học chính gồm mô hình thành phần phân tách chủ động/thụ động có ràng buộc tài nguyên, lý thuyết giao diện thời gian thực biểu diễn bằng ôtômát khoảng, và khung hợp đồng thời gian - tài nguyên cùng ngôn ngữ đặc tả mẫu trên nền tảng UTP. Các kết quả nghiên cứu cung cấp cơ sở phương pháp luận và các thuật toán tự động hóa quan trọng giúp bảo đảm chất lượng, nâng cao độ tin cậy và kiểm soát tối ưu tài nguyên của phần mềm thời gian thực ngay từ giai đoạn thiết kế sớm.