arXivDaily arXiv每日学术速递 周一至周五更新
arXiv周末暂无论文更新,休息一下吧,周末愉快~~
arXiv 1305.7410cs.NIcs.LO
收藏

无线传感器网络Ad Hoc路由协议自动形式化验证研究综述

A Review of Automated Formal Verification of Ad Hoc Routing Protocols for Wireless Sensor Networks

Zhe Chen, Daqiang Zhang, Rongbo Zhu, Yinxue Ma, Ping Yin, Feng Xie

摘要:

本文综述了无线传感器网络的基础设施--adhoc路由协议的正确性证明的形式化验证方法。现有的技术分为两类:小规模网络上的验证和无界网络上的验证。由于验证过程中产生的状态空间有限,前者始终是全自动的,易于使用。然而,它不能证明所有情况下的正确性。后者可以提供一个基于无界网络抽象的完整证明。然而,它通常需要用户干预和验证方面的专业知识。对这两种方法的稳定性、无环性和无死锁性等关键性能进行了验证。总之,它们可以分别用于查找错误和证明正确性。我们相信,他们可以一起帮助正确的ad hoc路由协议的发展和可靠的实现。

英文摘要:

This paper surveys how formal verification can be used to prove the correctness of ad hoc routing protocols, which are fundamental infrastructure of wireless sensor networks. The existing techniques fall into two classes: verification on small-scale networks and verification on unbounded networks. The former one is always fully automatic and easy to use, thanks to the limited state space generated in verification. However, it cannot prove the correctness over all cases. The latter one can provide a complete proof based on abstractions of unbounded network. However, it usually needs user intervention and expertise in verification. The two kinds of technique are illustrated by verifications against some key properties such as stability, loop-freedom and deadlock-freedom. To conclude, they can be used to find faults and prove correctness, respectively. We believe that they can together aid the development of correct ad hoc routing protocols and their reliable implementations.

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑