Skip to main content
SpringerLink
Log in

Parameterized Verification of Ad Hoc Networks

  • Conference paper
CONCUR 2010 - Concurrency Theory (CONCUR 2010)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6269))

Included in the following conference series:

Abstract

We study decision problems for parameterized verification of a formal model of Ad Hoc Networks with selective broadcast and spontaneous movement. The communication topology of a network is represented as a graph. Nodes represent states of individual processes. Adjacent nodes represent single-hop neighbors. Processes are finite state automata that communicate via selective broadcast messages. Reception of a broadcast is restricted to single-hop neighbors. For this model we consider verification problems that can be expressed as reachability of configurations with one node (resp. all nodes) in a certain state from an initial configuration with an arbitrary number of nodes and unknown topology. We draw a complete picture of the decidability boundaries of these problems according to different assumptions on communication graphs, namely static, mobile, and bounded path topology.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abdulla, P.A., Čerāns, C., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: LICS 1996, pp. 313–321 (1996)

    Google Scholar 

  2. Abdulla, P.A., Čerāns, C., Jonsson, B., Tsay, Y.-K.: Algorithmic analysis of programs with well quasi-ordered domains. Inf. Comput. 160(1-2), 109–127 (2000)

    Article  MATH  Google Scholar 

  3. Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. Inf. Comput. 127(2), 91–101 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  4. Delzanno, G., Sangnier, A., Zavattaro, G.: Parameterized verification of Ad Hoc Networks (Extended version). DISI-TR-10-01 (June 2010), http://www.disi.unige.it/index.php?research/techrep

  5. Ding, G.: Subgraphs and well quasi ordering. J. of Graph Theory 16(5), 489–502 (1992)

    Article  MATH  Google Scholar 

  6. Emerson, E.A., Namjoshi, K.S.: On model checking for non-deterministic infinite-state systems. In: LICS 1998, pp. 70–80 (1998)

    Google Scholar 

  7. Ene, C., Muntean, T.: A broadcast based calculus for Communicating Systems. In: IPDPS 2001, p. 149 (2001)

    Google Scholar 

  8. Esparza, J., Finkel, A., Mayr, R.: On the verification of Broadcast Protocols. In: LICS 1999, pp. 352–359 (1999)

    Google Scholar 

  9. Esparza, J., Nielsen, M.: Decidability issues for Petri nets - a survey. Bulletin of the EATCS 52, 245–262 (1994)

    MATH  Google Scholar 

  10. Esparza, J.: Some applications of Petri Nets to the analysis of parameterised systems. Talk at WISP 2003 (2003)

    Google Scholar 

  11. Fehnker, A., van Hoesel, L., Mader, A.: Modelling and verification of the LMAC protocol for wireless sensor networks. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 253–272. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  12. Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! TCS 256(1-2), 63–92 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  13. Godskesen, J.C.: A calculus for Mobile Ad Hoc Networks. In: Murphy, A.L., Vitek, J. (eds.) COORDINATION 2007. LNCS, vol. 4467, pp. 132–150. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  14. Merro, M.: An observational theory for Mobile Ad Hoc Networks. Inf. Comput. 207(2), 194–208 (2009)

    Article  MATH  MathSciNet  Google Scholar 

  15. Meyer, R.: On boundedness in depth in the pi-calculus. In: IFIP TCS 2008, pp. 477–489 (2008)

    Google Scholar 

  16. Mezzetti, N., Sangiorgi, D.: Towards a calculus for wireless systems. ENTCS 158, 331–353 (2006)

    Google Scholar 

  17. Milner, R.: Communicating and mobile systems: the pi-calculus. Cambridge Univ. Press, Cambridge (1999)

    MATH  Google Scholar 

  18. Minsky, M.: Computation: finite and infinite machines. Prentice Hall, Englewood Cliffs (1967)

    MATH  Google Scholar 

  19. Prasad, K.V.S.: A Calculus of Broadcasting Systems. Sci. of Comp. Prog. 25(2-3), 285–327 (1995)

    Article  Google Scholar 

  20. Saksena, M., Wibling, O., Jonsson, B.: Graph grammar modeling and verification of Ad Hoc Routing Protocols. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 18–32. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  21. Singh, A., Ramakrishnan, C.R., Smolka, S.A.: A process calculus for Mobile Ad Hoc Networks. In: Lea, D., Zavattaro, G. (eds.) COORDINATION 2008. LNCS, vol. 5052, pp. 296–314. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  22. Singh, A., Ramakrishnan, C.R., Smolka, S.A.: Query-Based model checking of Ad Hoc Network Protocols. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 603–661. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  23. Wies, T., Zufferey, D., Henzinger, T.A.: Forward analysis of depth-bounded processes. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol. 6014, pp. 94–108. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Genova,  

    Giorgio Delzanno & Arnaud Sangnier

  2. University of Bologna,  

    Gianluigi Zavattaro

Authors
  1. Giorgio Delzanno
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Arnaud Sangnier
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Gianluigi Zavattaro
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Laboratoire Spécification et Vérification (LSV), ENS de Cachan & CNRS, 94235, Cachan cedex, France

    Paul Gastin

  2. LIAFA, Université Paris Diderot, 75205, Paris cedex, France

    François Laroussinie

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Delzanno, G., Sangnier, A., Zavattaro, G. (2010). Parameterized Verification of Ad Hoc Networks. In: Gastin, P., Laroussinie, F. (eds) CONCUR 2010 - Concurrency Theory. CONCUR 2010. Lecture Notes in Computer Science, vol 6269. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15375-4_22

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-15375-4_22

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-15374-7

  • Online ISBN: 978-3-642-15375-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation