I. Giới thiệu
Luận văn thạc sĩ này tập trung vào việc ứng dụng mô hình Petri Net nâng cao để kiểm chứng mạng cảm ứng không dây. Mục tiêu chính là giải quyết vấn đề tắc nghẽn trong mạng cảm ứng không dây (WSN), một vấn đề nghiêm trọng gây mất gói tin và tiêu thụ năng lượng quá mức. Mô hình Petri Net được sử dụng để mô hình hóa và phân tích WSN, đặc biệt là Coloured Petri Nets (CPNs), một kỹ thuật mạnh mẽ kết hợp Petri Nets và ngôn ngữ lập trình. CPNs cho phép mô hình hóa các thông số và hành vi của WSN một cách hiệu quả, đồng thời hỗ trợ kiểm chứng hệ thống thông qua các kỹ thuật phân tích mạng và kiểm tra mô hình.
1.1 Tổng quan vấn đề
Mạng cảm ứng không dây (WSN) là một ứng dụng quan trọng trong công nghệ mạng, đặc biệt trong các môi trường khắc nghiệt như núi lửa, rừng rậm. Tuy nhiên, tắc nghẽn là một thách thức lớn, gây mất gói tin và tiêu thụ năng lượng quá mức. Luận văn thạc sĩ này đề xuất sử dụng mô hình Petri Net nâng cao, cụ thể là Coloured Petri Nets (CPNs), để mô hình hóa và kiểm chứng mạng nhằm phát hiện và kiểm soát tắc nghẽn. CPNs được chọn vì khả năng mô hình hóa phân cấp và biểu diễn tham số, giúp dễ dàng xử lý và mở rộng mô hình.
1.2 Mục tiêu của đề tài
Mục tiêu chính của luận văn thạc sĩ là sử dụng mô hình Petri Net nâng cao để kiểm chứng mạng cảm ứng không dây, đặc biệt là phát hiện tắc nghẽn. Các mục tiêu cụ thể bao gồm: nghiên cứu lý thuyết CPNs, xây dựng mô hình WSN, đề xuất phương pháp kiểm chứng mạng, và thực hiện kiểm tra mô hình bằng công cụ CPN Tools. Luận văn cũng nhằm mục đích cải thiện kết quả kiểm chứng hệ thống thông qua việc mở rộng mô hình để thể hiện tính đồng thời của WSN.
II. Nghiên cứu liên quan
Chương này trình bày các nghiên cứu liên quan đến mô hình hóa mạng và kiểm chứng mạng bằng Petri Nets. Các công cụ giả lập như OMNeT++ và ns-2 được sử dụng để mô phỏng WSN, nhưng chúng có hạn chế về khả năng mô phỏng và phụ thuộc vào khung chương trình. Mô hình hóa hình thức bằng Petri Nets được đề xuất như một giải pháp thay thế, đặc biệt là Coloured Petri Nets (CPNs), cho phép mô hình hóa các thông số và hành vi của WSN một cách trừu tượng và hiệu quả hơn.
2.1 Công cụ giả lập mạng cảm ứng không dây
Các công cụ giả lập như OMNeT++ và ns-2 được sử dụng rộng rãi để mô phỏng mạng cảm ứng không dây (WSN). Tuy nhiên, chúng có hạn chế về khả năng mô phỏng tất cả các tình huống và phụ thuộc vào khung chương trình. Luận văn thạc sĩ này đề xuất sử dụng mô hình hóa hình thức bằng Petri Nets, đặc biệt là Coloured Petri Nets (CPNs), để khắc phục những hạn chế này. CPNs cho phép mô hình hóa các thông số và hành vi của WSN một cách trừu tượng, giúp dễ dàng kiểm chứng mạng và phân tích mạng.
2.2 Mô hình và kiểm chứng mạng cảm ứng không dây bằng Petri Nets
Petri Nets đã được sử dụng để mô hình hóa và kiểm chứng mạng cảm ứng không dây (WSN). Tuy nhiên, các mô hình truyền thống như Place/Transition Nets (P/T Nets) có hạn chế về sức mạnh mô hình. Luận văn thạc sĩ này đề xuất sử dụng Coloured Petri Nets (CPNs), một loại Petri Nets nâng cao, để mô hình hóa WSN. CPNs kết hợp Petri Nets và ngôn ngữ lập trình, cho phép biểu diễn tham số và mô hình hóa phân cấp, giúp dễ dàng kiểm chứng hệ thống và phân tích mạng.
III. Kiến thức nền
Chương này cung cấp các kiến thức nền tảng về mạng cảm ứng không dây (WSN), Petri Nets, và Coloured Petri Nets (CPNs). WSN bao gồm các nút cảm biến và kênh truyền, hoạt động trong môi trường không dây. Petri Nets là một công cụ mạnh mẽ để mô hình hóa các hệ thống đồng thời, trong khi CPNs là một phiên bản nâng cao, kết hợp Petri Nets và ngôn ngữ lập trình. CPNs cho phép mô hình hóa phân cấp và biểu diễn tham số, giúp dễ dàng kiểm chứng hệ thống và phân tích mạng.
3.1 Mạng cảm ứng không dây
Mạng cảm ứng không dây (WSN) bao gồm các nút cảm biến và kênh truyền, hoạt động trong môi trường không dây. Các nút cảm biến thu thập dữ liệu và truyền về trạm giám sát. WSN được sử dụng rộng rãi trong các ứng dụng như giám sát môi trường, theo dõi hoạt động núi lửa, và quản lý rừng. Tuy nhiên, tắc nghẽn là một vấn đề nghiêm trọng trong WSN, gây mất gói tin và tiêu thụ năng lượng quá mức. Luận văn thạc sĩ này tập trung vào việc sử dụng mô hình Petri Net nâng cao để kiểm chứng mạng và phát hiện tắc nghẽn.
3.2 Coloured Petri Nets
Coloured Petri Nets (CPNs) là một phiên bản nâng cao của Petri Nets, kết hợp Petri Nets và ngôn ngữ lập trình. CPNs cho phép mô hình hóa các hệ thống phức tạp, đặc biệt là mạng cảm ứng không dây (WSN), bằng cách biểu diễn tham số và mô hình hóa phân cấp. CPNs cũng hỗ trợ kiểm chứng hệ thống thông qua các kỹ thuật phân tích mạng và kiểm tra mô hình. Luận văn thạc sĩ này sử dụng CPNs để mô hình hóa WSN và phát hiện tắc nghẽn, nhằm cải thiện hiệu quả kiểm chứng mạng.
