×

Modeling and efficient verification of wireless ad hoc networks. (English) Zbl 1377.68028


MSC:

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 arXiv

References:

[1] Abdulla PA, Delzanno G, Rezine O, Sangnier A, Traverso R (2011) On the verification of timed ad hoc networks. In: 9th international conference on formal modeling and analysis of timed systems, volume 6919 of LNCS, Springer, pp 256-270 · Zbl 1348.68115
[2] Rebeca formal modeling language. http://www.rebeca-lang.org/wiki/pmwiki.php/Tools/Afra
[3] Agha GA (1990) ACTORS—a model of concurrent computation in distributed systems. MIT Press series in artificial intelligence. MIT Press, Cambridge, MA · Zbl 1386.68019
[4] Bertsekas DP, Gallager RG (1992) Data networks. Prentice Hall, Upper Saddle River, NJ · Zbl 1185.68142
[5] Borgström J, Huang S, Johansson M, Raabjerg P, Victor B, Pohjola JÅ, Parrow J (2015) Broadcast psi-calculi with an application to wireless protocols. Softw Syst Model 14(1): 201-216 · Zbl 1350.68041 · doi:10.1007/s10270-013-0375-z
[6] Basler Gérard, Mazzucchi Michele, Wahl Thomas, Kroening Daniel (2009) Symbolic counter abstraction for concurrent software. In Computer Aided Verification, Springer pp 64-78 · Zbl 1242.68055
[7] Bhargavan K, Obradovic D, Gunter CA (2002) Formal verification of standards for distance vector routing protocols. J ACM 49(4): 538-576 · Zbl 1326.68039 · doi:10.1145/581771.581775
[8] Cui T, Chen L, Ho T (2007) Distributed optimization in wireless networks using broadcast advantage. In: Decision and control. IEEE, pp 5839-5844
[9] Clarke EM, Emerson EA, Jha S, Sistla AP (1998) Symmetry reductions in model checking. In: Hu AJ, Vardi MY (eds) Computer aided verification. Springer, Berlin, pp 147-158
[10] Dechter R, Kleinrock L (1986) Broadcast communications and distributed algorithms. IEEE Trans Comput 35(3): 210-219 · doi:10.1109/TC.1986.1676745
[11] De Renesse R, Aghvami AH (2004) Formal verification of ad-hoc routing protocols using spin model checker. In 12th IEEE mediterranean, electrotechnical conference, volume 3. IEEE, pp 1177-1182
[12] Delzanno G, Sangnier A, Traverso R, Zavattaro G (2012) On the complexity of parameterized reachability in reconfigurable broadcast networks. In: Annual conference on foundations of software technology and theoretical computer science, volume 18 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, pp 289-300 · Zbl 1354.68014
[13] Delzanno G, Sangnier A, Zavattaro G (2011) Parameterized verification of safety properties in ad hoc network protocols. In: First international workshop on process algebra and coordination, volume 60 of EPTCS, pp 56-65 · Zbl 1326.68040
[14] De Nicola R, Vaandrager FW (1990) Action versus state based logics for transition systems. In: Semantics of systems of concurrent processes, volume 469 of Lecture notes in computer science. Springer, pp 407-419
[15] Ene C, Muntean T (1999) Expressiveness of point-to-point versus broadcast communications. In: Ciobanu G, Păun G (eds) Fundamentals of computation theory. FCT 1999, volume 1684 of LNCS. Springer, Berlin · Zbl 0946.68096
[16] Emerson EA, Trefler RJ (1999) From asymmetry to full symmetry: new techniques for symmetry reduction in model checking. In: Pierre L, Kropf T (eds) Correct hardware design and verification methods. Springer, Berlin, pp 142-156 · Zbl 0957.68067
[17] Fehnker A, van Glabbeek R, Höfner P, McIver A, Portmann M, Tan WL (2012) Automated analysis of AODV using Uppaal. In: Tools and algorithms for the construction and analysis of systems, volume 7214 of LNCS. Springer, Berlin, pp 173-187 · Zbl 1386.68019
[18] Fehnker A, Van Glabbeek R, Höfner P, McIver A, Portmann M, Tan WL (2013) A process algebra for wireless mesh networks used for modelling, verifying and analysing AODV. arXiv preprint arXiv:1312.7645 · Zbl 1352.68183
[19] Ghassemi F, Ahmadi S, Fokkink W, Movaghar A (2013) Model checking MANETs with arbitrary mobility. In: Arbab F, Sirjani M (eds) Fundamentals of software engineering. Springer, Berlin, pp 217-232 · Zbl 1434.68299
[20] Ghassemi F, Fokkink W, Movaghar A (2008) Restricted broadcast process theory. In: Sixth IEEE international conference on software engineering and formal methods (SEFM). IEEE Computer Society, pp 345-354
[21] Ghassemi F, Fokkink W, Movaghar A (2011) Verification of mobile ad hoc networks: an algebraic approach. Theor Comput Sci 412(28): 3262-3282 · Zbl 1216.68160 · doi:10.1016/j.tcs.2011.03.017
[22] Godskesen JC (2007) A calculus for mobile ad hoc networks. In: Murphy AL, Vitek J (eds) Coordination models and languages, volume 4467 of LNCS. Springer, Berlin, pp 132-150 · Zbl 1292.68108
[23] Godskesen JC (2009) A calculus for mobile ad-hoc networks with static location binding. Electr Notes Theor Comput Sci 242(1): 161-183 · Zbl 1291.68286 · doi:10.1016/j.entcs.2009.06.018
[24] Godskesen JC (2010) Observables for mobile and wireless broadcasting systems. In: Coordination models and languages, volume 6116 of LNCS. Springer, Berlin, pp 1-15
[25] Hewitt C (1977) Viewing control structures as patterns of passing messages. Artif Intell 8(3): 323-364 · doi:10.1016/0004-3702(77)90033-9
[26] Jaghoori MM, Sirjani M, Mousavi MR, Khamespanah E, Movaghar A (2010) Symmetry and partial order reduction techniques in model checking Rebeca. Acta Inform 47(1): 33-66 · Zbl 1185.68142 · doi:10.1007/s00236-009-0111-x
[27] Katoen J-P (2011) Model checking: one can do much more than you think! In: Arbab F, Sirjani M (eds) Fundamentals of software engineering. Springer, Berlin, pp 1-14 · Zbl 1026.68098
[28] Kuhn F, Lynch NA, Newport CC (2011) The abstract MAC layer. Distrib Comput 24(3-4): 187-206 · Zbl 1231.68085 · doi:10.1007/s00446-010-0118-0
[29] Khamespanah E, Sirjani M, Sabahi-Kaviani Z, Khosravi R, Izadi M (2015) Timed rebeca schedulability and deadlock freedom analysis using bounded floating time transition system. Sci Comput Program 98: 184-204 · doi:10.1016/j.scico.2014.07.005
[30] Merro M (2009) An observational theory for mobile ad hoc networks (full version). Inf Comput 207(2):194-208, Special issue on Structural Operational Semantics (SOS) · Zbl 1165.68052
[31] Mclver AK, Fehnker A (2006) Formal techniques for the analysis of wireless networks. In: Second international symposium on leveraging applications of formal methods, verification and validation. IEEE, pp 263-270 · Zbl 1291.68286
[32] Mahmud SA, Khan S, Khan S, Al-Raweshidy H (2006) A comparison of manets and wmns: commercial feasibility of community wireless networks and manets. In: 1st international conference on access networks. ACM · Zbl 1273.68264
[33] Mateescu R, Sighireanu M (2003) Efficient on-the-fly model-checking for regular alternation-free mu-calculus. Sci Comput Program 46(3): 255-281 · Zbl 1026.68098 · doi:10.1016/S0167-6423(02)00094-1
[34] Mezzetti N, Sangiorgi D (2006) Towards a calculus for wireless systems. Electr Notes Theor Comput Sci 158(0): 331-353 · Zbl 1273.68264 · doi:10.1016/j.entcs.2006.04.017
[35] Nanz S, Hankin C (2006) A framework for security analysis of mobile wireless networks. Theor Comput Sci 367(1-2): 203-227 · Zbl 1153.68322 · doi:10.1016/j.tcs.2006.08.036
[36] Namjoshi KS, Trefler RJ (2015a) Analysis of dynamic process networks. In: Baier C, Tinelli C (eds) Tools and algorithms for the construction and analysis of systems, volume 9035 of LNCS. Springer, Berlin, pp 164-178
[37] Namjoshi KS, Trefler RJ (2015b) Loop freedom in aodvv2. In: Graf S, Viswanathan M (eds) Formal techniques for distributed objects, components, and systems, volume 9039 of LNCS. Springer, Cham, pp 98-112 · Zbl 1185.68142
[38] Perkins CE, Belding-Royer EM (1999) Ad-hoc on-demand distance vector routing. In: 2nd workshop on mobile computing systems and applications. IEEE Computer Society, Washington, DC, pp 90-100
[39] Pohjola JÅ, Borgström J, Parrow J, Raabjerg P (2013) Negative premises in applied process calculi. Technical report, Department of Information Technology, Uppsala University · Zbl 1342.68239
[40] Peng J (2008) A new arq scheme for reliable broadcasting in wireless lans. IEEE Commun Lett 12(2): 146-148 · doi:10.1109/LCOMM.2008.071275
[41] Plotkin GD (1981) A structural approach to operational semantics. Technical Report DAIMI FN-19, University of Aarhus
[42] Pnueli A, Xu J, Zuck LD (2002) Liveness with (0, 1, infty)-counter abstraction. In: 14th international conference on computer aided verification, CAV ’02, Springer, pp 107-122 · Zbl 1010.68095
[43] Reynisson AH, Sirjani M, Aceto L, Cimini M, Jafari A, Ingólfsdóttir A, Sigurdarson SH (2014) Modelling and simulation of asynchronous real-time systems using Timed Rebeca. Sci Comput Program 89:41-68 · Zbl 1231.68085
[44] Sirjani M, Jaghoori MM (2011) Ten years of analyzing actors: Rebeca experience. In: Agha G, Meseguer J, Danvy O (eds) Formal modeling: actors, open systems, biological systems. Springer, Berlin, pp 20-56
[45] Sabouri H, Khosravi R (2013) Delta modeling and model checking of product families. In: Arbab F, Sirjani M (eds) Fundamentals of software engineering. Springer, Berlin, pp 51-65 · Zbl 1434.68114
[46] Si W, Li C (2004) RMAC: A reliable multicast MAC protocol for wireless ad hoc networks. In: 33rd international conference on parallel processing (ICPP 2004). IEEE Computer Society, pp 494-501
[47] Sirjani M, Movaghar A, Shali A, de Boer FS (2004) Modeling and verification of reactive systems using Rebeca. Fundam Inform 63(4): 385-410 · Zbl 1082.68007
[48] Singh A, Ramakrishnan CR, Smolka SA (2010) A process calculus for mobile ad hoc networks. Sci Comput Program 75(6): 440-469 · Zbl 1192.68451 · doi:10.1016/j.scico.2009.07.008
[49] Sabouri H, Sirjani M (2010) Slicing-based reductions for rebeca. Electr Notes Theor Comput Sci 260: 209-224 · Zbl 1214.68223 · doi:10.1016/j.entcs.2009.12.039
[50] Saksena M, Wibling O, Jonsson B (2008) Graph grammar modeling and verification of ad hoc routing protocols. In: 14th international conference on tools and algorithms for the construction and analysis of systems, volume 4963 of LNCS. Springer, pp 18-32 · Zbl 1134.68418
[51] van Glabbeek RJ, Höfner P, Portmann M, Tan WL (2016) Modelling and verifying the AODV routing protocol. Distrib Comput 29(4): 279-315 · Zbl 1386.68019 · doi:10.1007/s00446-015-0262-7
[52] van Glabbeek R, Weijland WP (1996) Branching time and abstraction in bisimulation semantics. J ACM 43(3): 555-600 · Zbl 0882.68085 · doi:10.1145/233551.233556
[53] Varshosaz M, Khosravi R (2012) Modeling and verification of probabilistic actor systems using pRebeca. In: Aoki T, Taguchi K (eds) Formal methods and software engineering. Springer, Berlin, pp 135-150 · Zbl 1350.68041
[54] Wibling O, Parrow J, Pears A (2004) Automatized verification of ad hoc routing protocols. In: de Frutos-Escrig D, Núñez M (eds) Formal techniques for networked and distributed systems, volume 3235 of LNCS. Springer, Berlin, pp 343-358 · Zbl 1110.68327
[55] Wibling O, Parrow J, Pears A (2005) Ad hoc routing protocol verification through broadcast abstraction. In: Wang F (ed) Formal techniques for networked and distributed systems-FORTE 2005. Springer, Berlin, pp 128-142 · Zbl 1169.68328
[56] Yousefi B, Ghassemi F, Khosravi R (2015) Modeling and efficient verification of broadcasting actors. In: In pre-proceeding of 6th IPM international conference on fundamentals of software engineering, pp 114-128
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.