Formal verification of ad-hoc routing protocols using SPIN model checker

Formal verification of ad-hoc routing protocols using SPIN model checker
复制标题

使用 SPIN 模型检查器对自组织路由协议进行形式化验证

DOI：
10.1109/melcon.2004.1348275
复制
发表时间：
2004
期刊：
Proceedings of the 12th IEEE Mediterranean Electrotechnical Conference (IEEE Cat. No.04CH37521)
影响因子：
--
通讯作者：
Arnold Neville Pears
Arnold Neville Pears
中科院分区：
--
文献类型：
--
作者：
Oskar Wibling;J. Parrow;Arnold Neville Pears

文献摘要

被引文献

相似文献

测试和仿真是用于ad-hoc网络路由协议的唯一验证技术。尽管这些技术为我们提供了一个很好的协议行为的概述，但协议的一些不希望的方面仍然没有被发现。因此，需要进行正式核查。本文提出了一种新的技术，正式验证这样的协议，通过使用一个著名的模型检查器：SPIN。作为一个例子，无线自适应路由协议（W.A.R.P）的形式化验证已经执行。
Tests and simulations are the only verification techniques used for ad-hoc network routing protocols. Although these techniques give us an excellent overview of the protocol behavior, some undesirable aspects of the protocol could still be undiscovered. Therefore formal verification is needed. This paper presents a new technique to formally verify such protocols by the use of a well-known model-checker: SPIN. As an example, a formal verification of the wireless adaptive routing protocol (W.A.R.P) has been performed.