I. Khám phá luận văn về hệ thống lai thời gian thực kết nối đồng bộ
Luận văn thạc sĩ với chủ đề "Thẩm định các thành phần của hệ thống lai thời gian thực kết nối đồng bộ dựa trên logic tính toán khoảng DC" là một công trình nghiên cứu chuyên sâu, giải quyết bài toán phức tạp trong lĩnh vực công nghệ phần mềm. Trọng tâm của nghiên cứu là phát triển một hệ thống chứng minh có tính kết hợp (Compositional Proof System) để xác minh và thẩm định các hệ thống lai thời gian thực (real-time hybrid systems). Các hệ thống này, còn được biết đến là hệ thống cyber-physical, tích hợp cả các thành phần tính toán rời rạc và các quy trình vật lý liên tục. Chúng đóng vai trò cốt lõi trong nhiều ứng dụng đòi hỏi an toàn cao như hệ thống điều khiển hàng không, nhà máy điện hạt nhân, và đặc biệt là hệ thống điều khiển tàu điện. Luận văn đề xuất một phương pháp tiếp cận mới, mở rộng từ bộ ba Hoare cổ điển và sử dụng một biến thể của Logic Tính toán Khoảng là WDC* (Weakly Monotonic Time Extension of Duration Calculus). Lợi thế chính của phương pháp này là khả năng chia một hệ thống lớn, phức tạp thành các thành phần nhỏ hơn, dễ quản lý hơn. Việc chứng minh tính đúng đắn của toàn bộ hệ thống được suy ra từ tính đúng đắn của từng thành phần. Điều này giúp giải quyết hiệu quả vấn đề bùng nổ không gian trạng thái, một thách thức cố hữu trong các phương pháp hình thức (formal methods) truyền thống. Nghiên cứu này không chỉ mang giá trị lý thuyết mà còn được minh họa qua một ứng dụng thực tiễn: kiểm chứng mô hình cho thuộc tính an toàn tránh xung đột trong Hệ Thống Điều Khiển Tàu Điện Châu Âu (ETCS).
1.1. Định nghĩa hệ thống lai thời gian thực và tầm quan trọng
Một hệ thống lai thời gian thực là một hệ thống phức tạp, trong đó các thuật toán điều khiển số (rời rạc) tương tác và chi phối các quy trình vật lý (liên tục). Sự tương tác này phải tuân thủ các ràng buộc thời gian nghiêm ngặt. Ví dụ, trong một hệ thống lái tự động, máy tính phải xử lý dữ liệu từ cảm biến và đưa ra lệnh điều khiển trong một khoảng thời gian cực ngắn để đảm bảo an toàn. Tầm quan trọng của các hệ thống này ngày càng tăng do sự phát triển của mạng lưới và khả năng tính toán. Chúng là nền tảng của các hệ thống nhúng thời gian thực và các hệ thống tự động hóa an toàn cao. Tuy nhiên, sự kết hợp giữa tính đồng thời, ràng buộc thời gian, và giao diện liên tục-rời rạc làm cho việc phát triển và thẩm định chúng trở nên vô cùng khó khăn. Một lỗi nhỏ trong các hệ thống này có thể gây ra những thảm họa nghiêm trọng, đe dọa tài sản và tính mạng con người. Do đó, việc có một phương pháp xác minh và thẩm định hiệu quả là yêu cầu cấp thiết.
1.2. Giới thiệu Logic Tính toán Khoảng DC Duration Calculus
Duration Calculus (DC) là một logic thời gian thực được thiết kế để đặc tả và lý giải về các yêu cầu của hệ thống lai. Thay vì chỉ xem xét các sự kiện tại một thời điểm, DC cho phép lý giải về hành vi của hệ thống trong một khoảng thời gian. Khái niệm cốt lõi của DC là "duration" (khoảng thời gian), được ký hiệu là ∫S, đo lường tổng thời gian mà một trạng thái S tồn tại trong một khoảng quan sát. Luận văn này sử dụng một phiên bản mở rộng là DC* và WDC*. WDC* đặc biệt hữu ích vì nó hỗ trợ "giả thuyết đồng bộ lý tưởng" (true synchrony) và "tính toán siêu trù mật" (super-dense computation). Giả thuyết này coi các phép tính toán và giao tiếp là tức thời (không tốn thời gian), giúp đơn giản hóa đáng kể việc phân tích hành vi của hệ thống. Cách tiếp cận này giúp các nhà thiết kế tập trung vào logic điều khiển và các ràng buộc thời gian thực mà không bị sa đà vào các chi tiết phức tạp của việc mô hình hóa độ trễ tính toán.
II. Phân tích thách thức trong thẩm định hệ thống lai thời gian thực
Việc xác minh và thẩm định phần mềm cho các hệ thống lai thời gian thực đối mặt với nhiều thách thức to lớn, cản trở quá trình đảm bảo độ tin cậy và an toàn. Thách thức đầu tiên và lớn nhất là sự phức tạp vốn có của hệ thống. Mỗi tác tử thành phần có thể là một hệ thống lai với nhiều chế độ hoạt động và các biến đổi liên tục khác nhau, dẫn đến sự bùng nổ không gian trạng thái khi phân tích. Các phương pháp kiểm chứng mô hình truyền thống thường không có khả năng mở rộng để xử lý các hệ thống quy mô lớn. Thứ hai, việc phát triển một ngôn ngữ đặc tả hình thức có khả năng mô hình hóa thời gian một cách chính xác vẫn là một nhiệm vụ khó khăn. Các logic như Explicit Clock Temporal Logic hay Duration Calculus cổ điển, khi không sử dụng sự trừu tượng hóa của đồng bộ lý tưởng, làm cho việc lý giải hành vi hệ thống trở nên rất phức tạp. Cuối cùng, một vấn đề nan giải là sự không nhất quán giữa mô hình liên tục được sử dụng trong giai đoạn đặc tả yêu cầu và mô hình rời rạc được sử dụng trong giai đoạn cài đặt. Giao diện giữa thế giới vật lý liên tục và bộ điều khiển số rời rạc cần được hình thức hóa một cách chặt chẽ để đảm bảo rằng chương trình cài đặt thực sự đáp ứng các yêu cầu an toàn đã đề ra. Luận văn này trực tiếp giải quyết những thách thức này bằng cách đề xuất một hệ thống chứng minh có tính kết hợp, giúp giảm thiểu độ phức tạp và bắc cầu qua khoảng cách giữa đặc tả và cài đặt.
2.1. Vấn đề bùng nổ không gian trạng thái trong kiểm chứng
Bùng nổ không gian trạng thái là hiện tượng số lượng trạng thái có thể có của một hệ thống tăng theo cấp số nhân với số lượng thành phần hoặc biến. Trong các hệ thống cyber-physical, mỗi thành phần song song, mỗi biến liên tục, và mỗi ràng buộc thời gian đều góp phần làm tăng kích thước không gian trạng thái. Các phương pháp kiểm chứng truyền thống (non-compositional) yêu cầu phân tích toàn bộ hệ thống như một khối duy nhất. Điều này nhanh chóng trở nên bất khả thi đối với các hệ thống thực tế. Ví dụ, một hệ thống điều khiển tàu điện bao gồm nhiều tàu, mỗi tàu có trạng thái riêng (vị trí, tốc độ) và tương tác với nhau. Việc phân tích tất cả các kịch bản tương tác có thể xảy ra là một bài toán tính toán khổng lồ. Cách tiếp cận có tính kết hợp (compositional) được đề xuất trong luận văn giúp phá vỡ rào cản này bằng cách cho phép kiểm chứng từng thành phần một cách độc lập.
2.2. Khoảng cách giữa mô hình liên tục và cài đặt rời rạc
Một trong những thách thức cốt lõi trong nghiên cứu hệ thống điều khiển là sự khác biệt cơ bản giữa thế giới vật lý và thế giới số. Các đặc tả an toàn thường được diễn tả bằng các biến liên tục (như vị trí, vận tốc). Tuy nhiên, chương trình điều khiển chạy trên máy tính lại hoạt động với các giá trị rời rạc, được lấy mẫu tại các thời điểm cụ thể. Luận văn giải quyết sự không nhất quán này bằng cách hình thức hóa giao diện rời rạc. Các khái niệm như "tính ổn định" (stability), "trạng thái điều khiển" (control state) và "trạng thái quan sát" (observation state) được định nghĩa để mô hình hóa mối quan hệ giữa biến liên tục của môi trường và biến rời rạc trong bộ điều khiển. Điều này cho phép chứng minh một cách chặt chẽ rằng một chương trình điều khiển rời rạc có thể đảm bảo các thuộc tính an toàn của hệ thống vật lý liên tục, với các giả định hợp lý về độ trễ của cảm biến và cơ cấu chấp hành.
III. Phương pháp hình thức hóa hệ thống lai bằng Logic Khoảng DC
Để giải quyết các thách thức đã nêu, luận văn đề xuất một phương pháp hình thức mạnh mẽ dựa trên sự mở rộng của Logic Tính toán Khoảng. Cụ thể, nghiên cứu sử dụng WDC* (Phép Tính Toán Khoảng Có Lặp Với Thời Gian Đơn Điệu Yếu) để xây dựng ngữ nghĩa cho các chương trình thời gian thực. WDC* là một công cụ lý tưởng cho việc mô hình hóa các hệ thống lai thời gian thực kết nối đồng bộ. Điểm nổi bật của WDC* là nó cho phép tham số hóa logic với một khung thời gian vĩ mô (macro-time) và các điểm thời gian vi mô (micro-time) trong mỗi bước vĩ mô. Điều này hỗ trợ hoàn hảo cho giả thuyết "tính toán siêu trù mật", nơi nhiều bước tính toán rời rạc có thể xảy ra tại cùng một thời điểm vĩ mô. Bằng cách này, WDC* cung cấp một cơ sở lý thuyết vững chắc để đơn giản hóa việc lý giải về hành vi của hệ thống. Thay vì phải xử lý các độ trễ tính toán phức tạp, nhà thiết kế có thể tập trung vào logic tuần tự của các sự kiện. Luận văn trình bày chi tiết cú pháp và ngữ nghĩa của WDC*, bao gồm các tiên đề và luật suy diễn, đặc biệt là các luật liên quan đến toán tử lặp (*), vốn rất quan trọng để mô hình hóa các vòng lặp trong chương trình. Phương pháp này tạo ra một cầu nối logic giữa đặc tả hệ thống và việc cài đặt chương trình, đảm bảo tính nhất quán và đúng đắn.
3.1. Vai trò của WDC trong mô hình hóa thời gian đơn điệu yếu
Thời gian đơn điệu yếu (Weakly Monotonic Time) là một khái niệm quan trọng trong WDC*. Nó cho phép thời gian "dừng lại" ở cấp độ vĩ mô trong khi nhiều sự kiện vi mô (micro-steps) xảy ra. Mỗi điểm thời gian vi mô bao gồm một thời điểm vĩ mô và một pha đếm, thể hiện số bước tính toán đã diễn ra. Mô hình này rất phù hợp để mô tả các hệ thống lai thời gian thực, nơi các sự kiện tính toán (như gán biến, giao tiếp) xảy ra tức thời, xen kẽ với các giai đoạn mà thời gian trôi đi (như câu lệnh delay). WDC* cung cấp các toán tử và tiên đề để lý giải về cả khoảng thời gian vĩ mô (l) và số bước vi mô (η). Ví dụ, tiên đề AXM khẳng định rằng trong một khoảng thời gian vĩ mô bằng không (l=0), chỉ có một số hữu hạn các bước vi mô có thể xảy ra. Điều này giúp tránh các hành vi Zeno (vô hạn hành động trong thời gian hữu hạn) và cung cấp một nền tảng logic chặt chẽ cho logic thời gian thực.
3.2. Cách tiếp cận đồng bộ lý tưởng và tính toán siêu trù mật
Giả thuyết đồng bộ lý tưởng (true synchrony) là một trong những đóng góp cốt lõi của phương pháp này. Nó giả định rằng các hoạt động tính toán và giao tiếp qua các kênh không tốn thời gian. Chỉ có các lệnh chờ đợi rõ ràng (ví dụ delay) hoặc chờ đồng bộ hóa mới làm thời gian trôi đi. Điều này đơn giản hóa đáng kể mô hình hệ thống, cho phép các nhà phát triển tập trung vào logic và sự tương tác giữa các thành phần. Khái niệm tính toán siêu trù mật (super-dense computation) là hệ quả của giả thuyết trên, cho phép nhiều hành động tính toán xảy ra tại cùng một thời điểm. WDC* cung cấp các công cụ formal methods để biểu diễn và lý giải về các hành vi này một cách chính xác. Ví dụ, hai tiến trình song song có thể trao đổi thông điệp và cập nhật trạng thái của chúng tại cùng một điểm thời gian vĩ mô, được phân biệt bằng các bước thời gian vi mô khác nhau. Cách tiếp cận này giúp việc phân tích đồng bộ hóa dữ liệu trở nên trực quan và dễ quản lý hơn.
IV. Hướng dẫn kiểm chứng hệ thống lai với bộ ba Hoare mở rộng
Trọng tâm của kỹ thuật thẩm định trong luận văn kỹ thuật máy tính này là việc mở rộng bộ ba Hoare (Hoare triples) cổ điển để áp dụng cho các hệ thống lai thời gian thực. Bộ ba Hoare truyền thống {pre} P {post} chỉ lý giải về tính đúng đắn chức năng của chương trình. Phiên bản mở rộng có dạng {pre} [P, ϕ] {post}. Trong đó, ϕ là một công thức của Duration Calculus, mô tả hành vi thời gian của chương trình P trong quá trình thực thi. Công thức này có nghĩa là: nếu điều kiện trước pre đúng và chương trình P kết thúc, thì điều kiện sau post sẽ đúng và hành vi của P phải thỏa mãn đặc tả thời gian ϕ. Luận văn cũng định nghĩa một dạng thứ hai {pre} [P, ϕ] {} để xử lý các chương trình không dừng, một đặc tính phổ biến của các hệ thống điều khiển. Dựa trên bộ ba mở rộng này, một hệ thống chứng minh có tính kết hợp được xây dựng, bao gồm một tập hợp các luật kiểm chứng cho từng cấu trúc của ngôn ngữ lập trình (gán, tuần tự, lặp, song song, giao tiếp). Các luật này cho phép suy luận về tính đúng đắn của một chương trình phức tạp bằng cách phân tích các thành phần nhỏ hơn của nó. Đây chính là chìa khóa để thực hiện kiểm chứng mô hình một cách hiệu quả và có khả năng mở rộng.
4.1. Xây dựng hệ thống chứng minh có tính kết hợp hiệu quả
Một hệ thống chứng minh có tính kết hợp (compositional) cho phép chứng minh thuộc tính của một hệ thống lớn bằng cách kết hợp các chứng minh về các thành phần con của nó. Ví dụ, luật cho câu lệnh tuần tự P;Q cho phép suy ra thuộc tính của cả chuỗi lệnh từ các thuộc tính đã được chứng minh của P và Q. Tương tự, luật cho các tiến trình song song P1 || P2 cho phép kết hợp các đặc tả thời gian của P1 và P2 để suy ra hành vi của toàn bộ hệ thống. Luật 10 trong luận văn định nghĩa rõ ràng cách kết hợp các công thức duration của các tiến trình song song, với giả định rằng các lệnh delay sẽ chồng chéo lên nhau. Lợi ích của cách tiếp cận này là rất lớn: nó giúp quản lý sự phức tạp, cho phép tái sử dụng các chứng minh, và quan trọng nhất là tránh được vấn đề bùng nổ không gian trạng thái, giúp xác minh và thẩm định phần mềm trở nên khả thi cho các hệ thống quy mô công nghiệp.
4.2. Các luật kiểm chứng cho chương trình thời gian thực đồng bộ
Luận văn định nghĩa một tập hợp các luật kiểm chứng chi tiết cho một ngôn ngữ lập trình thời gian thực tương tự OCCAM, hỗ trợ các tiến trình song song và giao thức truyền thông đồng bộ qua kênh. Các luật này bao gồm: Luật 1 (Skip) và Luật 2 (Gán) xử lý các hành động tức thời. Luật 3 (Delay) giới thiệu ràng buộc thời gian l=d. Đặc biệt, Luật 4 (Output) và Luật 5 (Input) mô hình hóa việc giao tiếp đồng bộ, trong đó một tiến trình có thể phải chờ đợi (await) tiến trình kia sẵn sàng. Các luật cho cấu trúc điều khiển như Luật 7 (Tuần tự), Luật 8 (Điều kiện) và Luật 9 (Lặp) được xây dựng dựa trên các toán tử tương ứng trong Duration Calculus (toán tử chop ^, tuyển ∨, và lặp *). Các luật này cung cấp một bộ công cụ hình thức để các kỹ sư có thể từng bước xây dựng và chứng minh tính đúng đắn của chương trình điều khiển từ các yêu cầu ban đầu.
V. Ứng dụng thực tiễn Thẩm định hệ thống điều khiển tàu điện
Để minh họa tính hiệu quả và khả thi của phương pháp đề xuất, luận văn đã áp dụng nó vào một trường hợp nghiên cứu cụ thể và phức tạp: kiểm chứng mô hình cho việc tránh xung đột trong Hệ Thống Điều Khiển Tàu Điện Châu Âu (ETCS). Đây là một ví dụ điển hình về một hệ thống lai thời gian thực an toàn cao, nơi các quyết định điều khiển rời rạc của máy tính trên tàu và trung tâm điều khiển (RBC) ảnh hưởng trực tiếp đến chuyển động liên tục của tàu trên đường ray. Mục tiêu chính là chứng minh một thuộc tính an toàn cốt lõi: tàu không bao giờ di chuyển vượt qua điểm cuối của quyền di chuyển (End-of-Authority - EoA) và luôn giữ tốc độ trong giới hạn an toàn. Nghiên cứu đã mô hình hóa hệ thống ETCS thành ba tác tử chính: Plant (mô hình vật lý của tàu), Controller (bộ điều khiển trên tàu) và RBC. Quá trình thẩm định diễn ra theo các bước có cấu trúc: từ việc hình thức hóa yêu cầu hệ thống bằng công thức DC, đến việc thiết kế chiến lược điều khiển, sau đó là thiết kế rời rạc và cuối cùng là viết và kiểm chứng chương trình điều khiển. Kết quả cho thấy phương pháp này có thể được sử dụng để phân tích và đảm bảo các thuộc tính an toàn quan trọng trong một nghiên cứu hệ thống điều khiển thực tế.
5.1. Tổng quan về Hệ thống Điều khiển Tàu điện Châu Âu ETCS
ETCS là một chuẩn điều khiển tàu hiện đại, được thiết kế để đảm bảo an toàn và tăng khả năng tương tác giữa các hệ thống đường sắt ở Châu Âu. Nguyên tắc cơ bản của ETCS là cấp phát "quyền di chuyển" động cho mỗi tàu. Thay vì phân chia đường ray thành các khối cố định, RBC liên tục theo dõi vị trí của các tàu và cấp cho mỗi tàu một vùng an toàn phía trước, kết thúc tại điểm EoA. Bộ điều khiển trên tàu (ATP) có nhiệm vụ giám sát vị trí và tốc độ, đảm bảo tàu có thể phanh và dừng lại an toàn trước khi đến EoA. Khi tàu tiếp cận EoA, nó sẽ liên lạc với RBC để xin mở rộng quyền di chuyển. Việc mô hình hóa và kiểm chứng hệ thống này là một thách thức lớn do sự tương tác phức tạp giữa nhiều tàu, sự không chắc chắn trong giao tiếp không dây và các ràng buộc thời gian thực nghiêm ngặt.
5.2. Quy trình kiểm chứng thuộc tính an toàn tránh xung đột
Quy trình kiểm chứng trong luận văn được thực hiện một cách có hệ thống. Đầu tiên, yêu cầu an toàn Req ≙ □(0 ≤ v ≤ vdes ∧ 0 ≤ z ≤ m) được hình thức hóa, khẳng định rằng tại mọi thời điểm, vận tốc v và vị trí z của tàu luôn nằm trong giới hạn cho phép. Tiếp theo, một quyết định thiết kế Des được đưa ra, mô tả chi tiết chiến lược điều khiển trong các pha khác nhau (pha "far", pha "negotiation"). Thiết kế này sau đó được "làm mịn" thành một thiết kế rời rạc ϕCont, hoạt động trên các biến được lấy mẫu như zd và vd. Cuối cùng, một chương trình PCont được viết để cài đặt ϕCont. Sử dụng các luật chứng minh đã phát triển, luận văn chứng minh rằng A ⊢ ϕSYS ⇒ Des và Des ⇒ Req, trong đó A là các giả định về môi trường. Điều này cho thấy chương trình cài đặt, dưới các giả định hợp lý, thực sự đảm bảo được yêu cầu an toàn ban đầu. Đây là một minh chứng mạnh mẽ cho năng lực của phương pháp hình thức trong việc thẩm định các hệ thống nhúng thời gian thực phức tạp.
VI. Kết luận và triển vọng cho nghiên cứu hệ thống điều khiển lai
Luận văn "Thẩm định các thành phần của hệ thống lai thời gian thực kết nối đồng bộ dựa trên logic tính toán khoảng DC" đã trình bày thành công một hệ thống chứng minh có tính kết hợp dựa trên WDC*. Phương pháp này cho phép chuyển đổi một cách có hệ thống từ một thiết kế trừu tượng trong DC* sang một chương trình điều khiển thời gian thực có thể kiểm chứng được. Đóng góp chính của nghiên cứu nằm ở việc mở rộng bộ ba Hoare để tích hợp hành vi thời gian thực và tận dụng sức mạnh của WDC* để đơn giản hóa việc lý giải thiết kế thông qua giả thuyết đồng bộ lý tưởng. Cách tiếp cận có tính kết hợp đã chứng tỏ hiệu quả trong việc phân tách một hệ thống lớn thành các phần nhỏ dễ quản lý, từ đó vượt qua rào cản về bùng nổ không gian trạng thái trong các phương pháp hình thức truyền thống. Việc áp dụng thành công vào bài toán điều khiển tàu điện ETCS đã khẳng định giá trị thực tiễn của nghiên cứu. Trong tương lai, hướng đi này mở ra nhiều triển vọng. Việc cải tiến logic WDC* để hỗ trợ thêm nhiều loại hệ thống lai thời gian thực khác nhau là một hướng phát triển tiềm năng. Bên cạnh đó, việc xây dựng các công cụ tự động hóa quá trình chuyển đổi và kiểm chứng, chẳng hạn như cài đặt sự chuyển đổi từ WDC* sang các logic khác như CSP-OZ-DC, sẽ giúp phương pháp này trở nên dễ tiếp cận và ứng dụng rộng rãi hơn trong ngành công nghiệp phát triển phần mềm cho các hệ thống an toàn cao.
6.1. Đóng góp chính của luận văn trong lĩnh vực công nghệ phần mềm
Đây là một luận văn kỹ thuật máy tính có những đóng góp quan trọng. Thứ nhất, nó cung cấp một cầu nối vững chắc giữa lý thuyết đặc tả hình thức và thực tiễn lập trình hệ thống thời gian thực. Bằng cách sử dụng WDC* và bộ ba Hoare mở rộng, luận văn đã hình thức hóa một quy trình thiết kế từ yêu cầu đến cài đặt. Thứ hai, hệ thống chứng minh có tính kết hợp giúp giải quyết hiệu quả vấn đề về khả năng mở rộng trong kiểm chứng mô hình, làm cho việc thẩm định các hệ thống công nghiệp lớn trở nên khả thi. Thứ ba, việc đơn giản hóa mô hình thời gian thông qua giả thuyết đồng bộ lý tưởng giúp giảm bớt gánh nặng nhận thức cho các nhà thiết kế hệ thống, cho phép họ tập trung vào các khía cạnh logic và an toàn quan trọng hơn. Những đóng góp này thúc đẩy việc áp dụng các phương pháp chặt chẽ trong việc phát triển các hệ thống đòi hỏi độ tin cậy tuyệt đối.
6.2. Hướng phát triển tương lai cho các phương pháp hình thức
Tương lai của các formal methods trong nghiên cứu hệ thống điều khiển phụ thuộc vào khả năng tự động hóa và tích hợp vào các quy trình phát triển phần mềm hiện đại. Hướng đi được đề cập trong luận văn, như việc cài đặt chuyển đổi sang CSP-OZ-DC, là một bước đi đúng đắn. Việc này cho phép tận dụng các công cụ kiểm chứng hiện có cho các logic khác. Một hướng khác là phát triển các thư viện và framework cho phép các lập trình viên viết mã có thể kiểm chứng được một cách tự nhiên hơn, thay vì phải là chuyên gia về logic hình thức. Ngoài ra, việc mở rộng các phương pháp này để xử lý các hệ thống có tính không xác định, học máy hoặc tương tác với con người là những lĩnh vực nghiên cứu đầy hứa hẹn, giúp đảm bảo an toàn cho thế hệ tiếp theo của các hệ thống cyber-physical thông minh và tự trị.
