کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
432606 688986 2016 33 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Modeling and analyzing mobile ad hoc networks in Real-Time Maude
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
Modeling and analyzing mobile ad hoc networks in Real-Time Maude
چکیده انگلیسی


• Formalize node mobility models in Real-Time Maude.
• Formalize wireless mobile ad hoc networks in Real-Time Maude.
• Illustrate the use of our framework on the AODV and LE protocols.
• Provide a framework for composing Real-Time Maude specifications.

Modeling and analyzing mobile ad hoc networks (MANETs) pose non-trivial challenges to formal methods. Time, geometry, communication delays and failures, mobility, and uni- and bidirectional wireless communication can interact in unforeseen ways that are hard to model and analyze by current process calculi and automatic formal methods. As a consequence, current analyses tend to abstract away these physical aspects, so that—although still quite useful in finding various errors—their simplifying assumptions can easily fail to model details of MANET behavior relevant to meet desired requirements. In this work we present a formal framework for the modeling and analysis of MANETS based on Real-Time Maude to address this challenge. Specifically, we show that our framework has good expressive power to model relevant aspects of MANETs, and good compositionality properties, so that a MANET protocol can be easily composed with various models of mobility and with other MANET protocols. We illustrate the use of our framework on two well-known MANET benchmarks: the AODV routing protocol and the leader election protocol of Vasudevan, Kurose, and Towsley. Our formal analysis has uncovered a spurious behavior in the latter protocol that is due to the subtle interplay between communication delays, node movement, and neighbor discovery. This behavior therefore cannot be found by analyses that abstract from node movement and communication delays.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Journal of Logical and Algebraic Methods in Programming - Volume 85, Issue 1, Part 1, January 2016, Pages 34–66
نویسندگان
, , ,