Thông tin chung:

Ngày nhận:19/09/2015

Ngày chấp nhận: 10/10/2015

Title:

Applying component-based abstraction to verify congestion on wireless sensor network by using Petri net

Từ khóa:

Mạng cảm ứng không dây, Phát hiện tắc nghẽn, Kỹ thuật trừu tượng hóa, mạng Petri

Keywords:

Wireless Sensor Network,Congestion Detection, Abstraction tecchnique, Petri net

ABSTRACT

Congestion detection and mitigation on wireless sensor networks has widely been pursued by the research community. Generally, wireless sensor network is deployed in dense or spare mode which has a specified strategy to detect and avoid congestion. However, the cost of implementation a wireless network is too huge so that the congestion verification should be done on the simulation before deployment in reality.

We address this problem by model checking approach. Wireless sensor network is modeled by Petri nets and their properties are verified by model checking. Moreover, we use the component-based abstraction technique to abstract the unused components when verifying congestion. Our ideas have fully been implemented as a tool known as WSN-PN, on which the experimental results proved the significant improvement on verification process.

TÓM TẮT

Phát hiện và xử lý tắc nghẽn trên mạng cảm ứng không dây là một vấn đề thu hút nhiều sự chú ý trong cộng đồng nghiên cứu. Về cơ bản, mạng cảm ứng không dây có thể triển khai ở chế độ mạng dày hoặc mạng thưa; mỗi chế độ này đòi hỏi một chiến lược tiếp cận khác nhau để phát hiện và xử lý nghẽn. Do chi phí triển khai một mạng cảm ứng không dây là khá lớn, vấn đề kiểm tra sự tắc nghẽn trên mạng cần được kiểm tra trên một mô hình máy tính trước khi triển khai thực tế.

Chúng tôi giải quyết vấn đề này bằng cách sử dụng hướng tiếp cận kiểm tra mô hình. Ngôn ngữ mạng Petri được sử dụng để biểu diễn và kiểm tra các tính chất của một mạng không dây. Hơn thế nữa, chúng tôi còn sử dụng kỹ thuật trừu tượng hóa dựa trên thành phần để có thể trừu tượng hóa các thành phần không cần thiết trên một mạng cảm ứng không dây khi cần kiểm tra tắc nghẽn theo các chế độ khác nhau. Nhờ đó, tốc độ xử lý của chúng tôi được tăng lên rất nhiều. Chúng tôi đã phát triển công cụ WSN-PN để hiện thực ý tưởng này. Kết quả thí nghiệm cho thấy WSN-PN có thể thu giảm đáng kể không gian trạng thái cần kiểm tra khi sử dụng trừu tượng hóa.