Verification of Directed Acyclic Ad Hoc Networks

详细信息    查看全文

• 作者：Parosh Aziz Abdulla (18)
  Mohamed Faouzi Atig (18)
  Othmane Rezine (18)
  
• 刊名：Lecture Notes in Computer Science
• 出版年：2013
• 出版时间：2013
• 年：2013
• 卷：7892
• 期：1
• 页码：209-224
• 全文大小：292KB
• 参考文献：1. Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.: General decidability theorems for infinite-state systems. In: LICS 1996, pp. 313鈥?21. IEEE Computer Society (1996)
  2. 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鈥?27. Springer, Heidelberg (2010) CrossRef
  3. 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鈥?55. Springer, Heidelberg (2011) CrossRef
  4. 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鈥?72. Springer, Heidelberg (2007) CrossRef
  5. Higman, G.: Ordering by divisibility in abstract algebras. Proc. London Math. Soc. (3)聽2(7), 326鈥?36 (1952) CrossRef
  6. Intanagonwiwat, C., Govindan, R., Estrin, D., Heidemann, J., Silva, F.: Directed diffusion for wireless sensor networking. IEEE/ACM Trans. Netw.聽11(1), 2鈥?6 (2003) CrossRef
  7. Levis, P., Patel, N., Culler, D.E., Shenker, S.: Trickle: A self-regulating algorithm for code propagation and maintenance in wireless sensor networks. In: NSDI, pp. 15鈥?8 (2004)
  8. Merro, M., Ballardin, F., Sibilio, E.: A timed calculus for wireless systems. Theor. Comput. Sci.聽412(47), 6585鈥?611 (2011) CrossRef
  9. Nanz, S., Hankin, C.: A framework for security analysis of mobile wireless networks. Theor. Comput. Sci.聽367(1-2), 203鈥?27 (2006) CrossRef
  10. Prasad, K.V.S.: A calculus of broadcasting systems. Sci. Comput. Program.聽25(2-3), 285鈥?27 (1995) CrossRef
  11. 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鈥?2. Springer, Heidelberg (2008) CrossRef
  12. 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鈥?19. Springer, Heidelberg (2009) CrossRef
  13. Singh, A., Ramakrishnan, C.R., Smolka, S.A.: A process calculus for mobile ad hoc networks. Sci. Comput. Program.聽75(6), 440鈥?69 (2010) CrossRef
  
• 作者单位：Parosh Aziz Abdulla (18)
  Mohamed Faouzi Atig (18)
  Othmane Rezine (18)
  
  18. Uppsala University, Sweden
  
• ISSN：1611-3349

文摘

We study decision problems for parameterized verification of a formal model of ad hoc networks. We consider a model in which the network is composed of a set of processes connected to each other through a directed acyclic graph. Vertices of the graph represent states of individual processes. Adjacent vertices represent single-hop neighbors. The processes are finite-state machines with local and synchronized broadcast transitions. Reception of a broadcast is restricted to the immediate neighbors of the sender process. The underlying connectivity graph constrains communication pattern to only one direction. This allows to model typical communication patterns where data is propagated from a set of central nodes to the rest of the network, or alternatively collected in the other direction. For this model, we consider decidability of the control state reachability (coverability) problem, defined over two classes of architectures, namely the class of all acyclic networks (for which we show undecidability) and that of acyclic networks with a bounded depth (for which we show decidability). The decision problems are parameterized both by the size and by the topology of the underlying network.