Tổng quan luận án

Luận án tiến sĩ chuyên ngành Khoa học máy tính (Mã số chuyên ngành: 64.01) của tác giả Lê Ngọc Kim Khánh, thực hiện tại Trường Đại học Bách Khoa – Đại học Quốc gia Thành phố Hồ Chí Minh dưới sự hướng dẫn của PGS. TS. Quản Thành Thơ và PGS. TS. Bùi Hoài Thắng (năm bảo vệ: 2022), có tiêu đề: "Một cách tiếp cận hình thức trong việc mô hình hóa tham số động cho bài toán kiểm tra tắc nghẽn trên mạng cảm biến không dây".

Trong bối cảnh bùng nổ của các ứng dụng Internet vạn vật (Internet of Things - IoT) như nhà thông minh, đô thị thông minh, mạng cảm biến không dây (Wireless Sensor Networks - WSNs) đóng vai trò thu thập và truyền dữ liệu. Một mạng WSN bao gồm hàng trăm đến hàng ngàn thiết bị cảm biến (sensor) có giá thành thấp, bộ nhớ nhỏ, nguồn năng lượng pin hữu hạn và năng lực tính toán hạn chế. Cấu tạo của một nút cảm biến gồm ba bộ phận: cảm ứng (sensing), xử lý dữ liệu (data processing) và thông tin liên lạc (communicating). Kiểm soát tắc nghẽn là một yêu cầu kỹ thuật quan trọng nhằm bảo đảm chất lượng dịch vụ (QoS), giảm thiểu việc mất gói tin và kéo dài tuổi thọ mạng. Quá trình kiểm soát gồm hai giai đoạn là phát hiện tắc nghẽn và giải quyết tắc nghẽn; trong đó, luận án tập trung vào giai đoạn phát hiện tắc nghẽn.

Khoảng trống nghiên cứu được tác giả xác định xuất phát từ những hạn chế của hai phương pháp phát hiện nghẽn hiện hành:

  • Phương pháp tiếp cận dựa trên mô phỏng (simulation-based) thông qua các công cụ như ns-2, ns-3, Omnet++: Việc lập trình các hoạt động mạng phụ thuộc hoàn toàn vào khung thức (framework) hỗ trợ (ví dụ khung thức mf hay inet trên Omnet++). Khi công cụ thay đổi khung thức, người dùng phải xây dựng lại toàn bộ mô hình. Đồng thời, mô phỏng không thể kiểm tra vét cạn toàn bộ các kịch bản thực thi.
  • Phương pháp tiếp cận dựa trên mô hình hóa hình thức (model-based) kết hợp kỹ thuật kiểm tra mô hình (Model Checking - MC): Cung cấp mức độ trừu tượng hóa cao, độc lập với khung thức và kiểm tra toàn diện không gian trạng thái. Tuy nhiên, phương pháp này gặp phải vấn đề bùng nổ không gian trạng thái (state space explosion), dẫn đến việc tiêu tốn tài nguyên tính toán và gây chậm trễ trong việc đưa ra kết luận kiểm tra. Mặt khác, các nghiên cứu mô hình hóa bằng mạng Petri (Petri Net - PN) trước đây phần lớn dừng lại ở mô hình tĩnh, chưa phản ánh được sự biến đổi liên tục theo thời gian của các tham số mạng trong môi trường thực tế.

Luận án đặt ra ba câu hỏi nghiên cứu:

  • (RQ1) Mô hình WSN cho bài toán phát hiện nghẽn đã được nghiên cứu và xây dựng thành mô hình trước đây hay chưa? Nếu có thì loại ngôn ngữ mô hình hóa nào đã được chọn và tại sao lại chọn loại ngôn ngữ đó?
  • (RQ2) Vấn đề bùng nổ không gian trạng thái là vấn đề thường gặp trong những bài toán áp dụng kỹ thuật MC, nếu xảy ra việc bùng nổ thì nghiên cứu này cần phải giải quyết như thế nào?
  • (RQ3) Mô hình WSN đề xuất là linh hoạt dễ dàng tùy biến hay là mô hình tĩnh? Nếu là mô hình tĩnh thì cần có đề xuất gì khi sơ đồ WSN thay đổi?

Nhằm trả lời ba câu hỏi trên, luận án xác định ba mục tiêu nghiên cứu cụ thể:

  • (OB1) Xây dựng mô hình mạng cảm biến không dây bằng ngôn ngữ hình thức Petri Net, bao gồm ngôn ngữ sơ cấp Place/Transition Nets (P/T Nets) và ngôn ngữ cao cấp Coloured Petri Net (CPN).
  • (OB2) Khắc phục gián tiếp vấn đề bùng nổ không gian trạng thái bằng thuật toán gom cụm hướng nghẽn (Congestion-oriented Clustering Algorithm - COCA), thuật toán gom cụm mờ nhiều tầng và thuật toán tìm kiếm định hướng (heuristic search).
  • (OB3) Xây dựng mô hình mạng cảm biến không dây tham số động cho phép tùy chỉnh và cập nhật liên tục các thông số mạng mà không cần thiết lập lại mô hình từ đầu.

Đối tượng nghiên cứu của luận án là bài toán phát hiện tắc nghẽn do tràn bộ đệm (buffer overflow) trên các cảm biến và kênh truyền trong mạng cảm biến không dây. Phạm vi nghiên cứu về không gian là mô hình mạng WSN tĩnh có cấu trúc liên kết hỗn hợp (mesh topology), với các tham số khởi tạo dựa trên công nghệ truyền dẫn ZigBee và các quy chuẩn thực nghiệm trong tài liệu chuyên ngành. Phạm vi về thời gian và dữ liệu thực nghiệm được hoàn thiện và công bố trong giai đoạn 2018–2022.

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 hướng nghiên cứu liên quan đến bài toán tắc nghẽn và mô hình hóa mạng:

Về nguyên nhân và thuật toán phát hiện nghẽn trên WSN:

  • Tác giả Wan và cộng sự (2003) đề xuất thuật toán CODA, xác định nghẽn dựa trên kích thước vùng nhớ đệm còn trống (ngưỡng đệm quy định là 30% trống, tương đương sử dụng tối đa 70% dung lượng) kết hợp giá trị ngưỡng gói tin (buffer threshold).
  • Tác giả nghiên cứu [34] sử dụng tỷ lệ giữa số gói tin gửi đi tại nút gửi và số gói tin nhận được tại nút nhận (tỷ lệ lớn hơn 1 báo hiệu tắc nghẽn).
  • Tác giả nghiên cứu [21] chỉ ra mối quan hệ giữa mật độ phân bố cảm biến và nguy cơ tắc nghẽn: mạng dày đặc dễ xảy ra đụng độ gói tin và quá tải bộ đệm, trong khi mạng thưa thớt có nguy cơ tràn đệm do độ trễ truyền dẫn cự ly xa.
  • Thuật toán SENTCP [35] phát hiện nghẽn tại các nút trung gian thông qua việc đo lường thời gian lưu chuyển và thời gian xử lý gói tin.
  • Các công trình [36, 37] ứng dụng hệ suy diễn mờ (fuzzy logic) với các biến ngõ vào gồm tỷ lệ gửi/nhận gói, dung lượng đệm trống và số lượng cảm biến nhàn rỗi.

Về mô hình hóa mạng bằng ngôn ngữ Petri Net:

  • Các mô hình tĩnh: Công trình [38] dùng CPN mô hình hóa mạng ATM (Asynchronous Transfer Mode) thông qua phân rã mô hình con và biểu diễn kiểu ứng dụng bằng màu sắc (Color). Tác giả nghiên cứu [39] dùng Petri Net kiểm tra mạng ad-hoc không dây mở rộng. Tác giả nghiên cứu [40] mô hình hóa thiết bị chuyển mạch (switch) để kiểm tra dung lượng hàng đợi và tỷ lệ mất gói. Bài báo [41] dùng CPN đánh giá giao thức S-MAC trên tầng MAC. Bài báo [43] sử dụng Timed Coloured Petri Net kiểm chứng tính đúng đắn của giao thức định tuyến AODV trong môi trường thực thi song song.
  • Các mô hình tham số động trong các lĩnh vực khác: Mô hình Petri Net mờ (Fuzzy Petri Net) trong [44] biểu diễn dữ liệu không chắc chắn bằng tập luật IF-THEN. Nghiên cứu [45] kết hợp học tự động và gom nhóm transition không xung đột để lập lịch tự động. Nghiên cứu [46] mô hình hóa quy trình vận chuyển rác theo thời gian thực bằng Petri Net, gán xác suất thực thi cho transition phụ thuộc vào tham số ngoại cảnh để phát hiện bế tắc (deadlock).

Về kỹ thuật gom cụm (Clustering):

  • Kỹ thuật gom cụm phân cấp bao gồm tiếp cận tích tụ AGNES (Agglomerative Nesting) và tiếp cận phân chia DIANA (Divisive Analysis) [51].
  • Các nghiên cứu gom cụm nhằm cân bằng tải nội cụm thông qua nút trưởng cụm (Cluster Head - CH) [52], hoặc tối ưu hóa năng lượng để kéo dài thời gian sống của mạng [53, 54].
  • Kỹ thuật gom cụm dựa trên mật độ như DBSCAN [55, 56] và DENCLUE.

Khoảng trống nghiên cứu được luận án giải quyết: Việc áp dụng Fuzzy Petri Net [44] hay máy học [45] để mô hình hóa tham số động đòi hỏi phải định nghĩa lại các lớp mạng Petri mới và dễ gây bùng nổ không gian trạng thái. Luận án khắc phục khoảng trống này bằng cách: (1) Tích hợp trực tiếp các tham số động (độ tin cậy của nút và kênh truyền) vào mô hình Coloured Petri Net chuẩn thông qua toán tử toán học cập nhật liên tục tại mỗi bước chuyển marking; (2) Giải quyết vấn đề bùng nổ không gian trạng thái ở hai cấp độ: cấp độ topo mạng bằng thuật toán gom cụm COCA (dựa trên nguyên lý DBSCAN) và cấp độ không gian trạng thái bằng thuật toán tìm kiếm heuristic.

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

Luận án sử dụng phương pháp hình thức (formal methods) làm nền tảng cốt lõi, cụ thể là lý thuyết mạng Petri và kỹ thuật kiểm tra mô hình:

  1. Lý thuyết Place/Transition Nets (P/T Nets): P/T Net là một đồ thị phân đôi có hướng được định nghĩa bởi bộ 5 thành phần: $$N = (P, T, F, W, M_0)$$ Trong đó:
  • $P = {p_1, p_2, \dots, p_m}$ là tập hữu hạn các vị trí (place).
  • $T = {t_1, t_2, \dots, t_n}$ là tập hữu hạn các bước chuyển (transition), thỏa mãn $P \cap T = \emptyset$.
  • $F \subseteq (P \times T) \cup (T \times P)$ là tập các cung có hướng (arc).
  • $W: F \to \mathbb{N}^+$ là hàm gán trọng số trên các cung.
  • $M_0: P \to \mathbb{N}$ là đánh dấu khởi tạo (initial marking).

Điều kiện kích hoạt và chuyển bước: Transition $t \in T$ được kích hoạt tại marking $M$ (ký hiệu $M [t\rangle$) khi và chỉ khi: $$\forall p \in P: M(p) \ge W(p, t)$$ Khi $t$ thực thi, marking mới $M'$ được sinh ra theo quy tắc: $$M'(p) = M(p) - W(p, t) + W(t, p)$$ Tập hợp tất cả các marking tới được từ $M_0$ tạo thành đồ thị tới được hay không gian trạng thái (reachability graph / state space), ký hiệu là $Reach(M_0)$.

  1. Lý thuyết Coloured Petri Net (CPN): CPN mở rộng từ Petri Net truyền thống kết hợp với ngôn ngữ lập trình hàm CPN-ML, được định nghĩa bởi bộ 9 thành phần: $$CPN = (P, T, F, \Sigma, V, C, G, E, I)$$ Trong đó: $\Sigma$ là tập hợp các tập màu (colour sets); $V$ là tập hợp các biến; $C: P \to \Sigma$ là hàm gán tập màu cho place; $G: T \to EX_P$ là hàm điều kiện logic (guard function); $E: F \to EX_P$ là hàm biểu thức cung (arc expression); $I: P \to EX_P$ là hàm khởi tạo. CPN cho phép định nghĩa các kiểu dữ liệu phức tạp cho token thông qua đa tập (multiset $S_{ms}$) và cơ chế kết hợp biến (binding element). Mô hình mạng Petri màu phân cấp (Hierarchical Coloured Petri nets - HCPNs) cho phép trừu tượng hóa mô hình thành các mô-đun con thông qua các vị trí cổng (In, Out, In/Out) và bước chuyển thay thế (substitution transitions).

  2. Kỹ thuật Kiểm tra mô hình (Model Checking): Kỹ thuật do Edmund Melson Clarke và cộng sự đề xuất năm 1982, thực hiện duyệt trên không gian trạng thái để xác minh một thuộc tính hệ thống có được thỏa mãn hay không. Thuật toán áp dụng phương pháp duyệt đồ thị theo chiều sâu (Depth First Search - DFS) hoặc theo chiều rộng (Breadth First Search - BFS), kết hợp kỹ thuật sinh không gian trạng thái linh hoạt theo nhu cầu (on-the-fly).

  3. Dữ liệu và cấu hình thực nghiệm: Tham số mạng được xây dựng dựa trên công nghệ truyền dẫn ZigBee (đối chiếu với WiFi và Bluetooth) và các thiết lập chuẩn từ công trình của Wan và cộng sự.

Thuộc tính / Công nghệ ZigBee WiFi Bluetooth
Băng tần 2,4 - 2,483 GHz 2,4 - 2,483 GHz 2,4 - 2,483 GHz
Tốc độ truyền (kbits/s) 250 11000 723,1
Thời gian pin hoạt động liên tục (giờ) 100 - 1000 0,5 - 5 1 - 10
Phạm vi ứng dụng điển hình Quan trắc môi trường, mạng diện rộng Dữ liệu đa phương tiện, tốc độ cao Thiết bị y tế cá nhân, khoảng cách ngắn

Cấu hình tham số khởi tạo cho các thành phần mạng cảm biến không dây:

  • Một cảm biến $s$ được mô tả bằng bộ tham số $s = {b, q, p, sr}$: kích thước bộ đệm ($b$), kích thước hàng đợi ($q$), tốc độ xử lý gói tin ($p$), tốc độ gửi gói tin ($sr$).
  • Một kênh truyền $c$ được mô tả bằng bộ tham số $c = {b_c, t}$: kích thước bộ đệm kênh truyền ($b_c$), tốc độ chuyển gói tin ($t$).
Loại thành phần mạng Tốc độ gửi ($sr$) (gói/s) Kích thước bộ đệm ($b, b_c$) (gói) Kích thước hàng đợi ($q$) (gói) Tốc độ xử lý ($p$) (gói/s) Tốc độ truyền tin ($t$) (gói/s)
Cảm biến nguồn 2 - 3 5 5 1 - 3 -
Cảm biến trung gian 1 - 3 5 5 1 - 3 -
Cảm biến đích 2 - 3 5 5 1 - 3 -
Kênh truyền - 5 - - 1 - 3

Các quy tắc (luật) chuyển tiếp gói tin trong mô hình WSN:

Tên luật Biểu thức điều kiện và cập nhật Diễn giải chức năng
sensor_to_channel $q > 0 \implies q = q - 1, b_c = b_c + 1$ Gửi gói tin từ hàng đợi cảm biến sang bộ đệm kênh truyền
channel_to_sensor $b_c > 0 \implies b_c = \max(0, b_c - 1), b = b + 1$ Chuyển gói tin từ bộ đệm kênh truyền vào bộ đệm cảm biến
sensor_processing $b > 0 \implies b = \max(0, b - 1), q = q + 1$ Xử lý nội bộ: chuyển gói tin từ bộ đệm sang hàng đợi cảm biến

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

Chương 1: Mở đầu

Chương 1 trình bày bối cảnh nghiên cứu về vai trò của WSN trong hệ sinh thái IoT và phân tích hai nguyên nhân vật lý gây tắc nghẽn: tốc độ gửi gói tin vượt quá năng lực tiếp nhận/xử lý và sự đụng độ gói tin trên đường truyền, dẫn tới cơ chế tràn bộ đệm. Tác giả tiến hành so sánh đối chiếu hai trường phái tiếp cận: phương pháp mô phỏng (dùng ns-2, ns-3, Omnet++) và phương pháp mô hình hóa hình thức dựa trên kiểm tra mô hình. Trên cơ sở đó, chương này xác định 3 câu hỏi nghiên cứu (RQ1–RQ3), 3 mục tiêu nghiên cứu (OB1–OB3), 5 đóng góp chính, tầm quan trọng, các giới hạn kỹ thuật của đề tài và bố cục tổng thể của toàn bộ luận án.

Chương 2: Kiến thức nền tảng và Tình hình nghiên cứu

Chương 2 hệ thống hóa cơ sở lý thuyết toán học về mạng Petri sơ cấp P/T Nets và mạng Petri cao cấp CPN, bao gồm cấu trúc phân cấp HCPN. Tác giả phân tích nguyên lý của kỹ thuật Kiểm tra mô hình (Clarke et al., 1982), phân biệt kiểm tra tường minh (explicit) và kiểm tra ẩn (implicit), cũng như kỹ thuật sinh trạng thái on-the-fly. Phần tổng quan tài liệu phân tích sâu các cơ chế phát hiện nghẽn hiện có (CODA, SENTCP, logic mờ), các ứng dụng của mạng Petri trong mô hình hóa mạng truyền thông (ATM, ad-hoc, S-MAC, AODV), các công trình xử lý tham số động trong lập lịch và hệ thống mờ, cùng các giải thuật gom cụm dữ liệu (AGNES, DIANA, DBSCAN, DENCLUE). Từ đó, luận án lập luận về sự cần thiết của việc kết hợp P/T Nets, CPN, gom cụm hướng nghẽn và tìm kiếm heuristic.

Chương 3: Xây dựng mô hình mạng cảm biến không dây bằng ngôn ngữ Place/Transition Nets

Chương 3 trình bày việc thiết lập mô hình WSN-PN dựa trên ngôn ngữ P/T Nets. Tác giả phân rã mạng thành các Thành phần con (Component - $Com$) độc lập gồm ba tập vị trí rời rạc: vị trí vào ($P_{in}$), vị trí ra ($P_{out}$) và vị trí trung gian ($P_{inter}$). Các thành phần đại diện cho cảm biến nguồn, cảm biến trung gian, cảm biến đích và các kênh truyền theo cơ chế unicast, multicast, broadcast. Các thành phần này được ghép nối thông qua các Kết nối (Connector). Để kiểm soát sự bùng nổ không gian trạng thái, tác giả đề xuất kỹ thuật trừu tượng hóa thành phần (trừu tượng hóa cảm biến, kênh truyền hoặc đồng thời cả hai). Thuộc tính tắc nghẽn được kiểm tra trên đồ thị tới được (Reachability graph); khi phát hiện trạng thái có $b$ hoặc $b_c$ vượt ngưỡng, mô hình tự động kết xuất chuỗi vết phản ví dụ (counterexample) để chứng minh đường dẫn gây nghẽn.

Chương 4: Tăng tốc phát hiện nghẽn trên mô hình mạng cảm biến không dây

Chương 4 tập trung giải quyết hiện tượng bùng nổ không gian trạng thái thông qua hai giải pháp:

  • Kỹ thuật gom cụm hướng nghẽn: Đề xuất thuật toán COCA (Congestion-oriented Clustering Algorithm) dựa trên nguyên lý mật độ của DBSCAN. COCA vận hành qua 2 giai đoạn: gom cụm dựa trên khoảng cách hình học và gom cụm dựa trên độ mất cân đối tốc độ truyền tin. Thuật toán tích hợp trong Khung thức phát hiện nghẽn nhanh FCDF (Fast Congestion Detection Framework). FCDF thực hiện đánh giá độ nghẽn của cụm, tiến hành kiểm tra nghẽn cục bộ (bằng cách khôi phục tạm thời nút nguồn/đích trong cụm) và kiểm tra nghẽn toàn phần (trừu tượng hóa cụm thành nút đơn và tạo liên kết giả). Tính đúng đắn của phương pháp được chứng minh bằng toán học.
  • Kỹ thuật tìm kiếm định hướng (heuristic search): Xây dựng không gian trạng thái tối thiểu để trích xuất tri thức định hướng, thiết lập bảng heuristic với hàm đánh giá $f$, từ đó dẫn dắt thuật toán tìm kiếm trên không gian trạng thái thực tiến nhanh về trạng thái nghẽn mục tiêu thay vì duyệt mù toàn bộ đồ thị.

Chương 5: Xây dựng mô hình mạng cảm biến không dây bằng ngôn ngữ Coloured Petri Net

Chương 5 chuyển đổi mô hình sang ngôn ngữ Coloured Petri Net (WSN-CPN). Việc sử dụng CPN giải quyết triệt để hạn chế của P/T Nets bằng cách gắn nhãn kiểu dữ liệu (colour sets) cho token gói tin, cho phép đặc tả tường minh các thuộc tính định danh gói, địa chỉ nguồn và đích. Mô hình áp dụng kiến trúc phân cấp HCPN, chia tách hệ thống thành các mô-đun chức năng: Top, Initialisation, Generate Packet, Internal Process, Receive Packet, Transmit Packet. Đặc biệt, mô hình WSN-CPN được thiết kế vận hành theo cơ chế song song (concurrent), phản ánh chân thực bản chất hoạt động đồng thời của các nút mạng cảm biến. Kết quả phân tích không gian trạng thái chứng minh mô hình song song loại bỏ hoàn toàn các trường hợp "nghẽn giả" vốn xuất hiện trong mô hình vận hành tuần tự.

Chương 6: Mô hình tham số động cho Mạng cảm biến không dây và xác suất phát hiện nghẽn

Chương 6 hoàn thiện mô hình động PDP-WSN-CPN bằng cách tích hợp các tham số biến thiên theo thời gian. Tác giả định nghĩa hàm độ tin cậy của cảm biến, độ tin cậy của kênh truyền và độ tin cậy của các thao tác vận hành nội tại (với đặc tính suy giảm dần theo thời gian hoạt động). Độ tin cậy chi phối xác suất chọn đường đi của gói tin tại mỗi nút mạng. Thay vì tái cấu trúc mạng Petri, tham số động được tích hợp trực tiếp dưới dạng biểu thức toán tử và cập nhật giá trị mới tại mỗi bước kích hoạt transition. Luận án xây dựng công thức tính toán xác suất nghẽn trên không gian trạng thái CPN. Kết quả thực nghiệm xác nhận mô hình xác định chính xác các điểm nghẽn thực sự và loại bỏ các cảnh báo nghẽn giả do sai số mô hình tĩnh.

Chương 7: Xây dựng công cụ mô hình mạng cảm biến không dây cho bài toán kiểm tra tắc nghẽn

Chương 7 trình bày thiết kế kiến trúc và hiện thực phần mềm công cụ CODE-WSN (Congestion Detection on Wireless Sensor Networks). Công cụ được xây dựng với cấu trúc hướng đối tượng, bao gồm các lớp quản lý topo mạng, lớp chuyển đổi sang mô hình Petri Net, lớp sinh không gian trạng thái và lớp tích hợp các giải thuật tối ưu. CODE-WSN cho phép người dùng cấu hình tham số mạng, tự động sinh mã P/T Nets hoặc CPN, thực thi thuật toán gom cụm COCA, tìm kiếm heuristic và trực quan hóa vết phản ví dụ khi phát hiện nghẽn. Tác giả tiến hành so sánh tính năng của CODE-WSN với các công cụ kiểm tra mô hình và giả lập mạng thông dụng để khẳng định tính khả dụng của công cụ.

Chương 8: Kết luận

Chương 8 tổng kết toàn bộ nội dung nghiên cứu, đối chiếu kết quả đạt được với các mục tiêu (OB1–OB3) ban đầu. Chương này chỉ rõ các giới hạn còn tồn đọng và đề xuất các hướng phát triển tiếp theo, bao gồm việc mở rộng mô hình cho mạng cảm biến di động và tích hợp toàn diện thông số năng lượng.

Phụ lục A: Thuật toán gom cụm mờ nhiều tầng trên mạng cảm biến không dây

Phụ lục A bổ sung giải pháp gom cụm mờ nhiều tầng (Fuzzy multi-level clustering) hỗ trợ cho bài toán tối ưu hóa topo. Tác giả trình bày chi tiết thuật toán bầy sóc bay SSA (Squirrel Search Algorithm) và thuật toán tối ưu cải tiến OSSA (Opposition-based SSA kết hợp cơ chế học đối lập ngẫu nhiên - Random opposition-based learning). Quy trình gom cụm mờ nhiều tầng được xây dựng nhằm phân cụm hiệu quả trên các không gian mạng cảm biến có quy mô lớn và mật độ biến động.

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

Luận án tổng kết năm đóng góp khoa học chính gắn liền với các công trình đã công bố của tác giả:

  1. Đề xuất mô hình WSN-PN bằng ngôn ngữ Place/Transition Nets: Xây dựng thành công mô hình mạng cảm biến không dây gồm hai thành phần độc lập là cảm biến và kênh truyền; áp dụng kỹ thuật trừu tượng hóa để kiểm tra thuộc tính tắc nghẽn và xuất phản ví dụ (được công bố trong các công trình [CT04], [CT05], [CT06], [CT12], [CT13]). Đóng góp này hoàn thành mục tiêu (OB1).
  2. Đề xuất mô hình WSN-CPN bằng ngôn ngữ Coloured Petri Net: Xây dựng mô hình phân cấp HCPN vận hành theo cơ chế song song, định nghĩa tường minh kiểu dữ liệu của token gói tin và loại bỏ hiện tượng nghẽn giả (công bố trong công trình [CT03]). Đóng góp này hoàn thành mục tiêu (OB1).
  3. Đề xuất hai thuật toán tăng tốc độ kiểm tra nghẽn: Phát triển thuật toán gom cụm hướng nghẽn COCA trong khung thức FCDF trên sơ đồ mạng và thuật toán tìm kiếm heuristic trên không gian trạng thái, kết hợp kỹ thuật gom cụm mờ nhiều tầng OSSA (công bố trong [CT01], [CT09], [CT10], [CT11]). Đóng góp này hoàn thành mục tiêu (OB2).
  4. Đề xuất mô hình tham số động PDP-WSN-CPN: Tích hợp tham số độ tin cậy biến thiên theo thời gian của nút và kênh truyền, bổ sung cách tính xác suất nghẽn nhằm nâng cao độ chính xác dự báo (công bố trong [CT02], [CT08]). Đóng góp này hoàn thành mục tiêu (OB3).
  5. Xây dựng công cụ phần mềm CODE-WSN: Hiện thực hóa toàn bộ các mô hình và thuật toán đề xuất thành một công cụ tích hợp, phục vụ quy trình kiểm tra tắc nghẽn tự động trên WSN (công bố trong [CT07]).

Về mặt giải pháp và kiến nghị thực tiễn, luận án kiến nghị áp dụng phương pháp hình thức trong giai đoạn thiết kế tiền khả thi của hệ thống mạng WSN/IoT. Việc kiểm tra thuộc tính nghẽn trên mô hình giúp các nhà thiết kế dự báo trước toàn bộ các kịch bản nghẽn tiềm ẩn, từ đó tối ưu hóa việc phân bổ dung lượng bộ đệm và điều chỉnh tốc độ truyền tin trước khi triển khai phần cứng thực tế.

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

Luận án tự xác định ba hạn chế kỹ thuật cụ thể:

  • Tất cả các mô hình Petri Net đề xuất đều đòi hỏi thông số đầu vào là một sơ đồ mạng (topo) cố định ban đầu. Trong trường hợp có cảm biến bị lỗi hoặc ngừng hoạt động trong quá trình vận hành, mô hình chưa có khả năng tự tổ chức (self-organization) để tự động tái tạo topo mới.
  • Tiêu chí phát hiện tắc nghẽn trong luận án chỉ tập trung vào việc tính toán kích thước vùng nhớ đệm còn trống (nguyên nhân tràn bộ đệm). Trong thực tế, tắc nghẽn còn có thể xuất phát từ sự đụng độ tín hiệu đường truyền hoặc suy hao gói do can nhiễu môi trường vật lý.
  • Tham số năng lượng pin của cảm biến bị tạm gác lại trong các mô hình ở Chương 3, Chương 4 và Chương 5 để tránh làm bùng nổ không gian trạng thái; tham số này mới chỉ được tích hợp bước đầu trong mô hình CPN ở Chương 6.

Hướng nghiên cứu tiếp theo được tác giả vạch ra gồm:

  • Nghiên cứu tích hợp các thuật toán tự tổ chức mạng (self-organization) nhằm tự động cấu hình lại mô hình Petri Net khi topo thay đổi động do nút mạng bị hỏng.
  • Mở rộng mô hình hình thức để phát hiện tắc nghẽn do nguyên nhân đụng độ gói tin và suy giảm chất lượng liên kết truyền thông.
  • Mô hình hóa toàn diện tham số tiêu thụ năng lượng của cảm biến xuyên suốt tất cả các giai đoạn kiểm tra mô hình.

Giá trị tham khảo

Luận án mang lại giá trị tham khảo thiết thực cho các nhóm đối tượng học thuật và ứng dụng kỹ thuật:

  • Nghiên cứu sinh, học viên cao học và giảng viên chuyên ngành Khoa học máy tính, Kỹ thuật phần mềm, Mạng máy tính: Luận án cung cấp phương pháp luận chi tiết về việc ứng dụng phương pháp hình thức (P/T Nets, CPN, Model Checking) vào bài toán mạng truyền thông, đặc biệt là kỹ thuật ánh xạ cấu trúc mạng thành các mô hình phân cấp và giải pháp tích hợp tham số động.
  • Kỹ sư thiết kế và hoạch định mạng IoT/WSN: Công trình cung cấp giải pháp tính toán, dự báo trước nguy cơ tắc nghẽn và kiểm chứng quy hoạch bộ đệm của cảm biến mà không cần đầu tư chi phí xây dựng hệ thống thử nghiệm vật lý.
  • Các phần đáng tham khảo sâu: Chương 4 với thuật toán COCA và khung thức FCDF (cung cấp giải pháp toán học thu gọn topo mạng); Chương 5 với thiết kế mô-đun CPN chạy song song; và Chương 6 với phương pháp tích hợp độ tin cậy suy giảm theo thời gian vào mô hình mạng Petri.

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

  1. Nguyên nhân chính gây tắc nghẽn trong mạng cảm biến không dây được luận án xác định là gì và độ đo phát hiện nghẽn là gì?
    Luận án xác định nguyên nhân kỹ thuật cốt lõi dẫn đến tắc nghẽn là do tràn bộ đệm (buffer overflow), xảy ra khi tốc độ gửi gói tin đến cảm biến hoặc kênh truyền vượt quá năng lực xử lý và chuyển tiếp gói tin của thiết bị. Độ đo được sử dụng để phát hiện nghẽn là kích thước vùng nhớ đệm còn trống (empty buffer size); trạng thái nghẽn được ghi nhận khi dung lượng sử dụng vượt quá ngưỡng cho phép (quy định ở mức 70% dung lượng bộ đệm, tức vùng nhớ trống dưới 30%).

  2. Thuật toán COCA giải quyết vấn đề bùng nổ không gian trạng thái theo nguyên lý nào?
    Thuật toán COCA (kết hợp trong khung thức FCDF) hoạt động trực tiếp trên sơ đồ mạng (topo) trước khi sinh không gian trạng thái. Vận dụng ý tưởng phân cụm mật độ của DBSCAN, COCA gom các cảm biến có nguy cơ nghẽn cao thành các cụm thông qua hai tiêu chí: khoảng cách hình học dày đặc và tốc độ truyền tin mất cân đối. Sau đó, hệ thống ưu tiên kiểm tra nghẽn cục bộ bên trong từng cụm; các cụm không nghẽn sẽ được trừu tượng hóa thành một nút mạng duy nhất với các liên kết giả để kiểm tra toàn phần. Cơ chế này làm giảm số lượng trạng thái phải duyệt qua trong quá trình kiểm tra mô hình.

  3. Tại sao tác giả phải chuyển đổi từ mô hình P/T Nets sang Coloured Petri Net (CPN)?
    Mặc dù P/T Nets có ưu điểm đơn giản và gần gũi với sơ đồ mạng, ngôn ngữ này chỉ hỗ trợ các token đồng nhất (chấm đen), không thể phân biệt dữ liệu giữa các gói tin. Ngược lại, CPN cho phép định nghĩa các tập màu (colour sets) để gắn kiểu dữ liệu tường minh cho gói tin (định danh, địa chỉ nguồn, địa chỉ đích). Hơn nữa, CPN hỗ trợ cấu trúc phân cấp (HCPN) giúp mô hình hóa hệ thống dưới dạng các mô-đun tái sử dụng và hỗ trợ cơ chế vận hành song song thực sự, giúp loại bỏ các trường hợp nghẽn giả.

  4. Hiện tượng "nghẽn giả" trong mô hình tuần tự là gì và được giải quyết như thế nào trong Chương 5?
    Trong mô hình vận hành tuần tự, các tiến trình xử lý gói tin của các nút mạng được kích hoạt lần lượt theo một thứ tự giả định. Sự chậm trễ mang tính nhân tạo này khiến các gói tin bị ứ đọng tạm thời tại hàng đợi của một số nút, làm bộ đệm bị đầy và kích hoạt cảnh báo nghẽn dù trong thực tế hệ thống không nghẽn. Bằng cách xây dựng mô hình WSN-CPN vận hành song song ở Chương 5, các thao tác nhận, xử lý và gửi gói tin của các cảm biến diễn ra đồng thời, từ đó phản ánh đúng trạng thái bộ đệm thực tế và triệt tiêu các cảnh báo nghẽn giả.

  5. Mô hình PDP-WSN-CPN xử lý tham số động độ tin cậy như thế nào mà không làm tái bùng nổ không gian trạng thái?
    Thay vì sử dụng mạng Petri mờ hay tích hợp các mô hình máy học phức tạp (vốn làm phình to cấu trúc mạng Petri), PDP-WSN-CPN tích hợp các tham số độ tin cậy (của cảm biến, kênh truyền và các tác vụ nội tại) dưới dạng các biểu thức toán học gán trực tiếp vào các cung và guard của transition. Giá trị độ tin cậy này suy giảm theo hàm thời gian và được tính toán, cập nhật tức thời tại mỗi bước chuyển marking ($M \to M'$). Cơ chế cập nhật động này giúp mô hình thích ứng linh hoạt mà không làm thay đổi cấu trúc đồ thị Petri Net ban đầu.

Kết luận

Luận án tiến sĩ của tác giả Lê Ngọc Kim Khánh đã giải quyết bài toán phát hiện tắc nghẽn trên mạng cảm biến không dây bằng phương pháp mô hình hóa hình thức dựa trên mạng Petri và kiểm tra mô hình. Công trình đã xây dựng thành công hệ thống mô hình từ sơ cấp (WSN-PN) đến cao cấp (WSN-CPN) và mô hình tham số động tích hợp độ tin cậy (PDP-WSN-CPN). Đồng thời, tác giả đã đề xuất các thuật toán tăng tốc kiểm tra mô hình hiệu quả thông qua gom cụm hướng nghẽn COCA và tìm kiếm heuristic, và hiện thực hóa toàn bộ đóng góp vào công cụ phần mềm CODE-WSN. Kết quả nghiên cứu cung cấp một cơ sở lý thuyết và công cụ thực thi hỗ trợ công tác quy hoạch, thiết kế mạng WSN/IoT trước khi triển khai thực địa.