×

Modeling and analyzing mobile ad hoc networks in Real-Time Maude. (English) Zbl 1356.68123

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

MSC:

68Q42 Grammars and rewriting systems
68M10 Network design and communication in computer systems
68M12 Network protocols
68Q60 Specification and verification (program logics, model checking, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Agha, G.; Meseguer, J.; Sen, K., PMaude: rewrite-based specification language for probabilistic object systems, Electron. Notes Theor. Comput. Sci., 153, 213-239 (2006)
[2] AlTurki, M.; Meseguer, J., PVeStA: a parallel statistical model checking and quantitative analysis tool, (Proc. CALCO’11. Proc. CALCO’11, Lecture Notes in Computer Science, vol. 6859 (2011), Springer)
[3] AlTurki, M.; Meseguer, J.; Gunter, C., Probabilistic modeling and analysis of DoS protection for the ASV protocol, Electron. Notes Theor. Comput. Sci., 234, 3-18 (2009)
[4] Bhargavan, K.; Obradovic, D.; Gunter, C., Formal verification of standards for distance vector routing protocols, J. ACM, 49, 538-576 (2002) · Zbl 1326.68039
[5] Bruni, R.; Meseguer, J., Semantic foundations for generalized rewrite theories, Theor. Comput. Sci., 360, 386-414 (2006) · Zbl 1097.68051
[6] Camp, T.; Boleng, J.; Davies, V., A survey of mobility models for ad hoc network research, Wirel. Commun. Mob. Comput., 2, 483-502 (2002)
[7] Cerone, A.; Hennessy, M.; Merro, M., Modelling MAC-layer communications in wireless systems, (Proc. COORDINATION’13. Proc. COORDINATION’13, Lecture Notes in Computer Science, vol. 7890 (2013), Springer)
[8] Chiyangwa, S.; Kwiatkowska, M. Z., A timing analysis of AODV, (Proc. FMOODS’05. Proc. FMOODS’05, Lecture Notes in Computer Science, vol. 3535 (2005), Springer)
[9] Clavel, M.; Durán, F.; Eker, S.; Lincoln, P.; Martí-Oliet, N.; Meseguer, J.; Talcott, C., All About Maude, Lecture Notes in Computer Science, vol. 4350 (2007), Springer
[10] Eckhardt, J.; Mühlbauer, T.; AlTurki, M.; Meseguer, J.; Wirsing, M., Stable availability under denial of service attacks through formal patterns, (Proc. FASE’12. Proc. FASE’12, Lecture Notes in Computer Science, vol. 7212 (2012), Springer)
[11] Fehnker, A.; van Glabbeek, R.; Höfner, P.; McIver, A.; Portmann, M.; Tan, W., A process algebra for wireless mesh networks used for modelling, verifying and analysing AODV, NICTA (2012), Technical Report 5513
[12] Fehnker, A.; van Glabbeek, R. J.; Höfner, P.; McIver, A.; Portmann, M.; Tan, W. L., Automated analysis of AODV using Uppaal., (Proc. TACAS’12. Proc. TACAS’12, Lecture Notes in Computer Science, vol. 7214 (2012), Springer), 173-187
[13] Gelastou, M.; Georgiou, C.; Philippou, A., On the application of formal methods for specifying and verifying distributed protocols, (NCA (2008), IEEE)
[14] Ghassemi, F.; Ahmadi, S.; Fokkink, W.; Movaghar, A., Model checking MANETs with arbitrary mobility, (Proc. FSEN’13. Proc. FSEN’13, Lecture Notes in Computer Science, vol. 8161 (2013), Springer) · Zbl 1434.68299
[15] Ghassemi, F.; Fokkink, W.; Movaghar, A., Restricted broadcast process theory, (Proc. SEFM ’08 (2008), IEEE)
[16] Ghassemi, F.; Talebi, M.; Movaghar, A.; Fokkink, W., Stochastic restricted broadcast process theory, (EPEW. EPEW, Lecture Notes in Computer Science, vol. 6977 (2011), Springer)
[17] Godskesen, J. C., A calculus for mobile ad hoc networks, (Proc. Coordination’07. Proc. Coordination’07, Lecture Notes in Computer Science, vol. 4467 (2007), Springer) · Zbl 1292.68108
[18] Godskesen, J. C.; Nanz, S., Mobility models and behavioural equivalence for wireless networks, (Proc. Coordination’09. Proc. Coordination’09, Lecture Notes in Computer Science, vol. 5521 (2009), Springer)
[19] Höfner, P.; Kamali, M., Quantitative analysis of AODV and its variants on dynamic topologies using statistical model checking, (Proc. FORMATS’13. Proc. FORMATS’13, Lecture Notes in Computer Science, vol. 8053 (2013), Springer)
[20] Katelman, M.; Meseguer, J.; Hou, J. C., Redesign of the LMST wireless sensor protocol through formal modeling and statistical model checking, (Proc. FMOODS’08. Proc. FMOODS’08, Lecture Notes in Computer Science, vol. 5051 (2008), Springer)
[21] Kouzapas, D.; Philippou, A., A process calculus for dynamic networks, (Proc. FMOODS/FORTE’11. Proc. FMOODS/FORTE’11, Lecture Notes in Computer Science, vol. 6722 (2011), Springer)
[22] Lepri, D.; Ábrahám, E.; Ölveczky, P. C., A timed CTL model checker for Real-Time Maude, (Proc. CALCO’13. Proc. CALCO’13, Lecture Notes in Computer Science, vol. 8089 (2013), Springer)
[23] Lepri, D.; Ábrahám, E.; Ölveczky, P. C., Sound and complete timed CTL model checking of timed Kripke structures and real-time rewrite theories, Sci. Comput. Program., 99, 128-192 (2015)
[24] Liu, S.; Ölveczky, P. C.; Meseguer, J., A framework for mobile ad hoc networks in Real-Time Maude, (Proc. WRLA’14. Proc. WRLA’14, Lecture Notes in Computer Science, vol. 8663 (2014), Springer) · Zbl 1356.68122
[25] Liu, S.; Ölveczky, P. C.; Meseguer, J., Formal analysis of leader election in MANETs using Real-Time Maude, (Software, Services, and Systems: Essays Dedicated to Martin Wirsing on the Occasion of His Retirement from the Chair of Programming and Software Engineering. Software, Services, and Systems: Essays Dedicated to Martin Wirsing on the Occasion of His Retirement from the Chair of Programming and Software Engineering, Lecture Notes in Computer Science, vol. 8950 (2015), Springer) · Zbl 1454.68014
[26] Merro, M., An observational theory for mobile ad hoc networks (full version), Inf. Comput., 207, 194-208 (2009) · Zbl 1165.68052
[27] Merro, M.; Ballardin, F.; Sibilio, E., A timed calculus for wireless systems, Theor. Comput. Sci., 412, 6585-6611 (2011) · Zbl 1227.68077
[28] Merro, M.; Sibilio, E., A calculus of trustworthy ad hoc networks, Form. Asp. Comput., 25, 801-832 (2013) · Zbl 1298.68041
[29] Meseguer, J., Conditional rewriting logic as a unified model of concurrency, Theor. Comput. Sci., 96, 73-155 (1992) · Zbl 0758.68043
[30] Meseguer, J., Membership algebra as a logical framework for equational specification, (Proc. WADT’97. Proc. WADT’97, Lecture Notes in Computer Science, vol. 1376 (1998), Springer) · Zbl 0903.08009
[31] Mezzetti, N.; Sangiorgi, D., Towards a calculus for wireless systems, Electron. Notes Theor. Comput. Sci., 158, 331-353 (2006) · Zbl 1273.68264
[32] Nanz, S.; Hankin, C., A framework for security analysis of mobile wireless networks, Theor. Comput. Sci., 367, 203-227 (2006) · Zbl 1153.68322
[33] Ölveczky, P. C., Real-Time Maude and its applications, (Proc. WRLA’14. Proc. WRLA’14, Lecture Notes in Computer Science, vol. 8663 (2014), Springer)
[34] Ölveczky, P. C.; Meseguer, J., Specification of real-time and hybrid systems in rewriting logic, Theor. Comput. Sci., 285, 359-405 (2002) · Zbl 1001.68061
[35] Ölveczky, P. C.; Meseguer, J., Semantics and pragmatics of Real-Time Maude, High.-Order Symb. Comput., 20, 161-196 (2007) · Zbl 1115.68095
[36] Ölveczky, P. C.; Thorvaldsen, S., Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in Real-Time Maude, Theor. Comput. Sci., 410, 254-280 (2009) · Zbl 1178.68699
[37] Perkins, C.; Belding-Royer, E.; Das, S., Ad hoc on-demand distance vector (AODV) routing (2003), RFC 3561 (experimental)
[38] Perkins, C. E.; Belding-Royer, E. M., Ad-hoc on-demand distance vector routing, (2nd Workshop on Mobile Computing Systems and Applications (WMCSA ’99) (1999), IEEE Computer Society), 90-100
[39] Ping, S., Delay measurement time synchronization for wireless sensor networks (2003), Intel Research Berkeley, Technical Report IRB-TR-03-013
[40] Rocha, C.; Meseguer, J.; Muñoz, C. A., Rewriting modulo SMT and open system analysis, (Proc. WRLA’14. Proc. WRLA’14, Lecture Notes in Computer Science, vol. 8663 (2014), Springer) · Zbl 1367.68151
[41] Sen, K.; Viswanathan, M.; Agha, G., On statistical model checking of stochastic systems, (Proc. CAV’05. Proc. CAV’05, Lecture Notes in Computer Science, vol. 3576 (2005), Springer) · Zbl 1081.68635
[42] Sibilio, E., Formal methods for wireless systems (2011), University of Verona, Ph.D. thesis
[43] Singh, A.; Ramakrishnan, C. R.; Smolka, S. A., A process calculus for mobile ad hoc networks, Sci. Comput. Program., 75, 440-469 (2010) · Zbl 1192.68451
[44] Song, L., Probabilistic models and process calculi for Mobile Ad hoc Networks (2012), IT University of Copenhagen, Ph.D. thesis
[45] Song, L.; Godskesen, J. C., Broadcast abstraction in a stochastic calculus for mobile networks, (Proc. IFIP TCS’12. Proc. IFIP TCS’12, Lecture Notes in Computer Science, vol. 7604 (2012), Springer) · Zbl 1362.68018
[46] Vasudevan, S.; Kurose, J. F.; Towsley, D. F., Design and analysis of a leader election algorithm for mobile ad hoc networks (2003), University of Massachusetts, Technical Report UMass CMPSCI 03-20
[47] Vasudevan, S.; Kurose, J. F.; Towsley, D. F., Design and analysis of a leader election algorithm for mobile ad hoc networks, (Proc. ICNP’04 (2004), IEEE)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.