TRỪU TƯỢNG HÓA DỰA TRÊN THÀNH PHẦN ĐỂ KIỂM TRA TẮC NGHẼN TRÊN MẠNG CẢM ỨNG KHÔNG DÂY SỬ DỤNG MẠNG PETRI

Lê Ngọc Kim Khánh * , Lê Quốc Vũ , Tân Quốc Tiến , Bùi Hoài Thắng và Quản Thành Thơ

* Tác giả liên hệ (lengockimkhanh_toasoanctu@gmail.com)

Article Sidebar

Full Text: PDF

Ngày nhận bài: 19-09-2015
Ngày duyệt đăng: 10-10-2015
Ngày xuất bản: 15-12-2015
Title: Applying component-based abstraction to verify congestion on wireless sensor network by using Petri net
Lượt xem
65
Downloads
38
Trích dẫn
Khánh, L. N. K., Vũ, L. Q., Tiến, T. Q., Thắng, B. H., & Thơ, Q. T. (2015). TRỪU TƯỢNG HÓA DỰA TRÊN THÀNH PHẦN ĐỂ KIỂM TRA TẮC NGHẼN TRÊN MẠNG CẢM ỨNG KHÔNG DÂY SỬ DỤNG MẠNG PETRI. Tạp chí Khoa học Đại học Cần Thơ, (CĐ Công nghệ TT), 105-112. Truy vấn từ https://ctujsvn.ctu.edu.vn/index.php/ctujsvn/article/view/2340
Số báo
Số. CĐ Công nghệ TT (2015)
Chuyên mục
Công nghệ thông tin

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.
Keywords: Wireless Sensor Network, Congestion Detection, Abstraction tecchnique, Petri net

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.  
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

Article Details

Tài liệu tham khảo

V. E. Kozura, V. A. Nepomniaschy, and R. M. Novikov, “Verification of distributed systems modelled by high-level petri nets”, in 2002 International Conference on Parallel Computing in Electrical Engineering (PARELEC 2002), 2002, pp. 61–66.

K. Schmidt, “Lola: A low level analyser”, in International Conference on Application and Theory of Petri Nets (ICATPN 2000), 2000, pp. 465–474.

M. Heiner, R. Richter, and M. Schwarick, “Snoopy: a tool to design and animate/simulate graph-based formalisms”, in Proceedings of the 1st International Conference on Simulation Tools and Techniques for Communications, Networks and Systems & Workshops (SimuTools 2008), 2008, p. 15.

D. Chiarugi, P. Degano, and R. Marangoni, “A computational approach to the functional screening of genomes”, PLoS Computational Biology, vol. 3, no. 9, 2007.

C. Baier and J. Katoen, Principles of model checking. MIT Press, 2008.

R. Kaivola, R. Ghughal, N. Narasimhan, A. Telfer, J. Whittemore, S. Pandav, A. Slobodová, C. Taylor, V. Frolov, E. Reeber, and A. Naik, “Replacing testing with formal verification in intel coretm i7 processor execution engine validation”, in Computer Aided Verification, 21st International Conference, (CAV 2009), 2009, pp. 414–429.

E. M. Clarke, D. E. Long, and K. L. McMillan, “Compositional modelchecking,” in Proceedings of the Fourth Annual Symposium on Logicin Computer Science (LICS ’89), 1989, pp. 353–362.

D. Peled, A. Valmari, and I. Kokkarinen, “Relaxed visibility enhances partial order reduction”, Formal Methods in System Design, vol. 19, no. 3, pp. 275–289, 2001.

W. Merro, E. Clarke, and S. Jha, “Model checking for security protocols”, CMU, 1997.

M. Zheng, J. Sun, Y. Liu, J. S. Dong, and Y. Gu, “Towards a model checker for nesc and wireless sensor networks”, in Formal Methods and Software Engineering - 13th International Conference on Formal Engineering Methods, ICFEM 2011, 2011, pp. 372–387.

I. F. Akyildiz, W. Su, Y. Sankarasubramaniam, and E. Cayirci, “Wireless sensor networks: a survey,” Computer Networks, vol. 38, no. 4, pp. 393–422, 2002.

S. Moon, S. Lee, and H. Cha, “A congestion control technique for the near-sink nodes in wireless sensor networks,” in Ubiquitous Intelligence and Computing, Third International Conference, UIC 2006, Wuhan, China, September 3-6, 2006, Proceedings, 2006, pp. 488–497.

C. Wan, S. B. Eisenman, and A. T. Campbell, “CODA: congestion detection and avoidance in sensor networks”, in Proceedings of the 1st International Conference on Embedded Networked Sensor Systems (SenSys 2003). ACM, 2003, pp. 266–279.

A. Varga and R. Hornig, “An overview of the OMNeT++ simulation environment”, in Proceedings of the 1st International Conference on Simulation Tools and Techniques for Communications, Networks and Systems & Workshops (SimuTools 2008), 2008, p. 60.

Y. Si, J. Sun, Y. Liu, J. S. Dong, J. Pang, S. J. Zhang, and X. Yang, “Model checking with fairness assumptions using PAT”, Frontiers of Computer Science, vol. 8, no. 1, pp. 1–16, 2014.