Model checking mobile ad hoc networks

详细信息    查看全文

• 作者：Fatemeh Ghassemi ; Wan Fokkink
• 关键词：Mobile ad hoc networks ; Model checking ; Multi ; hop network constraints ; Constrained labeled transition systems
• 刊名：Formal Methods in System Design
• 出版年：2016
• 出版时间：December 2016
• 年：2016
• 卷：49
• 期：3
• 页码：159-189
• 全文大小：
• 刊物类别：Engineering
• 刊物主题：Circuits and Systems; Electrical Engineering; Computer-Aided Engineering (CAD, CAE) and Design; Software Engineering/Programming and Operating Systems;
• 出版者：Springer US
• ISSN：1572-8102
• 卷排序：49

文摘

Modeling arbitrary connectivity changes within mobile ad hoc networks (MANETs) makes application of automated formal verification challenging. We use constrained labeled transition systems as a semantic model to represent mobility. To model check MANET protocols with respect to the underlying topology and connectivity changes, we introduce a branching-time temporal logic. The path quantifiers are parameterized by multi-hop constraints over topologies, to discriminate the paths over which the temporal behavior should be investigated; the paths that violate the multi-hop constraints are not considered. A model checking algorithm is presented to verify MANETs that allow arbitrary mobility, under the assumption of reliable communication. It is applied to analyze a leader election protocol.