Skip to main content
SpringerLink
Log in

On the Verification of Timed Ad Hoc Networks

  • Conference paper
Formal Modeling and Analysis of Timed Systems (FORMATS 2011)

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

Abstract

We study decidability and undecidability results for parameterized verification of a formal model of timed Ad Hoc network protocols. The communication topology is represented by a graph and the behavior of each node is represented by a timed automaton communicating with its neighbors via broadcast messages. We consider verification problems formulated in terms of reachability, starting from initial configurations of arbitrary size, of a configuration that contain at least one occurrence of a node in a certain state. We study the problem for dense and discrete time and compare the results with those obtained for (fully connected) networks of timed automata.

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 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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., Cerans, K., Jonsson, B., Tsay, Y.: General decidability theorems for infinite-state systems. In: LICS 1996, pp. 313–321. IEEE Computer Society, Los Alamitos (1996)

    Google Scholar 

  2. Abdulla, P., Delzanno, G., Rezine, O., Sangnier, A., Traverso, R.: On the verification of timed ad hoc networks. Disi-11-05. Univ. of Genova (July 2011)

    Google Scholar 

  3. Abdulla, P., Deneux, J., Mahata, P.: Multi-clock timed networks. In: LICS 2004, pp. 345–354. IEEE Computer Society, Los Alamitos (2004)

    Google Scholar 

  4. Abdulla, P., Nylén, A.: Timed petri nets and bqos. In: Colom, J.-M., Koutny, M. (eds.) ICATPN 2001. LNCS, vol. 2075, pp. 53–70. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  5. Abdulla, P.A., Deneux, J., Mahata, P.: Closed, open, and robust timed networks. ENTCS 138(3), 117–151 (2005)

    MathSciNet  MATH  Google Scholar 

  6. Abdulla, P.A., Jonsson, B.: Model checking of systems with many identical timed processes. TCS 290(1), 241–264 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  7. Delzanno, G., Sangnier, A., Zavattaro, G.: Parameterized verification of ad hoc networks. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 313–327. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  8. Delzanno, G., Sangnier, A., Zavattaro, G.: On the power of cliques in the parameterized verification of ad hoc networks. In: Hofmann, M. (ed.) FOSSACS 2011. LNCS, vol. 6604, pp. 441–455. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  9. Delzanno, G., Sangnier, A., Zavattaro, G.: Verification of ad hoc networks with node and communication failures. Disi-11-06. Univ. of Genova (July 2011)

    Google Scholar 

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

    Article  MathSciNet  MATH  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. Lazic, R., Newcomb, T., Ouaknine, J., Roscoe, A.W., Worrell, J.: Nets with tokens which carry data. Fund. Inf. 88(3), 251–274 (2008)

    MathSciNet  MATH  Google Scholar 

  13. Merro, M., Ballardin, F.F., Sibilio, E.: A timed calculus for wireless systems. In: Arbab, F., Sirjani, M. (eds.) FSEN 2009. LNCS, vol. 5961, pp. 228–243. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  14. Nanz, S., Nielson, F., Nielson, H.: Static analysis of topology-dependent broadcast networks. Inf. Comput. 208(2), 117–139 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  15. 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 

  16. 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–619. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  17. The uppaal web page, http://www.uppaal.com/

Download references

Author information

Authors and Affiliations

  1. Uppsala University, Sweden

    Parosh Aziz Abdulla & Othmane Rezine

  2. University of Genova, Italy

    Giorgio Delzanno & Riccardo Traverso

  3. Liafa-University Paris 7, France

    Arnaud Sangnier

Authors
  1. Parosh Aziz Abdulla
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Giorgio Delzanno
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Othmane Rezine
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Arnaud Sangnier
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Riccardo Traverso
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. IRISA/INRIA Rennes, Campus Beaulieu, 35042, Rennes Cedex, France

    Uli Fahrenberg

  2. University of California, 94720-1770, Berkeley, CA, USA

    Stavros Tripakis

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Abdulla, P.A., Delzanno, G., Rezine, O., Sangnier, A., Traverso, R. (2011). On the Verification of Timed Ad Hoc Networks. In: Fahrenberg, U., Tripakis, S. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2011. Lecture Notes in Computer Science, vol 6919. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24310-3_18

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-24310-3_18

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-642-24310-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation