Mechanized Extraction of Topology Anti-patterns in Wireless Networks

  • Matthias Woehrle
  • Rena Bakhshi
  • Mohammad Reza Mousavi
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7321)


Exhaustive and mechanized formal verification of wireless networks is hampered by the huge number of possible topologies and the large size of the actual networks. However, the generic communication structure in such networks allows for reducing the root causes of faults to faulty (sub-)topologies, called anti-patterns, of small size. We propose techniques to find such anti-patterns using a combination of model-checking and automated debugging. We apply the proposed technique on two well-known protocols for wireless sensor networks and show that the techniques indeed find the root causes in terms of canonical topologies featuring the fault.


Wireless Network Wireless Sensor Network Time Slot Model Check Medium Access Control Protocol 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abreu, R., Zoeteweij, P., Golsteijn, R., van Gemund, A.: A practical evaluation of spectrum-based fault localization. Journal of Systems and Software 82(11), 1780–1792 (2009)CrossRefGoogle Scholar
  2. 2.
    Bakhshi, R., Endrullis, J., Endrullis, S., Fokkink, W., Haverkort, B.: Automating the mean-field method for large dynamic gossip networks. In: Proc. Conf. on Quantitative Evaluation of SysTems (QEST), pp. 241–250. IEEE Computer Society (2010)Google Scholar
  3. 3.
    Behrmann, G., David, A., Larsen, K.G.: A Tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  4. 4.
    Beutel, J., Gruber, S., Hasler, A., Lim, R., Meier, A., Plessl, C., Talzi, I., Thiele, L., Tschudin, C., Woehrle, M., Yuecel, M.: PermaDAQ: A scientific instrument for precision sensing and data recovery in environmental extremes. In: Proc. 8th ACM/IEEE Int’l Conf. on Information Processing in Sensor Networks (IPSN 2009), pp. 265–276. ACM/IEEE, San Francisco, CA, USA (2009)Google Scholar
  5. 5.
    Cadilhac, M., Hérault, T., Lassaigne, R., Peyronnet, S., Tixeuil, S.: Evaluating complex MAC protocols for sensor networks with APMC. In: Proc. Workshop on Automated Verification of Critical Syst. (AVoCS 2006). ENTCS, vol. 185, pp. 33–46. Elsevier (2007)Google Scholar
  6. 6.
    Chaki, S., Groce, A., Strichman, O.: Explaining abstract counterexamples. In: Proceedings of the 12th ACM SIGSOFT Twelfth International Symposium on Foundations of Software Engineering, SIGSOFT 2004/FSE-12, pp. 73–82. ACM, New York (2004)CrossRefGoogle Scholar
  7. 7.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press (2000)Google Scholar
  8. 8.
    Clarke, E.M., Veith, H.: Counterexamples Revisited: Principles, Algorithms, Applications. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 208–224. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  9. 9.
    Emerson, E.A., Sistla, A.P.: Symmetry and model checking. Formal Methods in System Design 9(1/2), 105–131 (1996)CrossRefGoogle Scholar
  10. 10.
    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)CrossRefGoogle Scholar
  11. 11.
    Godefroid, P.: Using Partial Orders to Improve Automatic Verification Methods. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 176–185. Springer, Heidelberg (1991)CrossRefGoogle Scholar
  12. 12.
    Groce, A., Visser, W.: What Went Wrong: Explaining Counterexamples. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 121–135. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  13. 13.
    Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: A Tool for Automatic Verification of Probabilistic Systems. In: Hermanns, H. (ed.) TACAS 2006. LNCS, vol. 3920, pp. 441–444. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  14. 14.
    Ip, C.N., Dill, D.L.: Better verification through symmetry. Formal Methods in System Design 9(1/2), 41–75 (1996)Google Scholar
  15. 15.
    Kamali, M., Laibinis, L., Petre, L., Sere, K.: Self-recovering sensor-actor networks. In: Mousavi, M.R., Salaün, G. (eds.) FOCLASA. EPTCS, vol. 30, pp. 47–61 (2010)Google Scholar
  16. 16.
    Katoen, J.-P., Kemna, T., Zapreev, I., Jansen, D.N.: Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 87–101. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  17. 17.
    Katoen, J.-P., Klink, D., Leucker, M., Wolf, V.: Three-Valued Abstraction for Continuous-Time Markov Chains. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 311–324. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  18. 18.
    Khan, M.M.H., Le, H.K., Ahmadi, H., Abdelzaher, T.F., Han, J.: Dustminer: troubleshooting interactive complexity bugs in sensor networks. In: SenSys 2008: Proceedings of the 6th ACM Conference on Embedded Network Sensor Systems, pp. 99–112. ACM, New York (2008)CrossRefGoogle Scholar
  19. 19.
    Kwiatkowska, M., Norman, G., Parker, D.: Game-based abstraction for markov decision processes. In: Proc. Conf. on Quantitative Evaluation of SysTems (QEST), pp. 157–166. IEEE Computer Society (2006)Google Scholar
  20. 20.
    Laplante, S., Lassaigne, R., Magniez, F., Peyronnet, S., de Rougemont, M.: Probabilistic abstraction for model checking: An approach based on property testing. In: Proc. IEEE Symp. on Logic in Comput. Sci. (LICS 2002), pp. 30–39. IEEE Computer Society (2002)Google Scholar
  21. 21.
    Levis, P., Patel, N., Culler, D., Shenker, S.: Trickle: a self-regulating algorithm for code propagation and maintenance in wireless sensor networks. In: Proceedings of the 1st Conference on Symposium on Networked Systems Design and Implementation, vol. 1, p. 2. USENIX Association (2004)Google Scholar
  22. 22.
    Lorincz, K., Chen, B.-R., Challen, G.W., Chowdhury, A.R., Patel, S., Bonato, P., Welsh, M.: Mercury: a wearable sensor network platform for high-fidelity motion analysis. In: Proc. ACM Conf. on Embedded Networked Sensor Systems, SenSys 2009, pp. 183–196. ACM, New York (2009)CrossRefGoogle Scholar
  23. 23.
    Khan, M.M.H., Abdelzaher, T., Gupta, K.K.: Towards Diagnostic Simulation in Sensor Networks. In: Nikoletseas, S.E., Chlebus, B.S., Johnson, D.B., Krishnamachari, B. (eds.) DCOSS 2008. LNCS, vol. 5067, pp. 252–265. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  24. 24.
    Mottola, L., Voigt, T., Österlind, F., Eriksson, J., Baresi, L., Ghezzi, C.: Anquiro: enabling efficient static verification of sensor network software. In: Proc. ICSE Workshop on Software Engineering for Sensor Network Applications (SESENA), pp. 32–37. ACM, New York (2010)CrossRefGoogle Scholar
  25. 25.
    Peled, D.: All From One, One For All: on Model Checking Using Representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 409–423. Springer, Heidelberg (1993)CrossRefGoogle Scholar
  26. 26.
    Rodionov, A.S., Choo, H.: On Generating Random Network Structures: Trees. In: Sloot, P.M.A., Abramson, D., Bogdanov, A.V., Gorbachev, Y.E., Dongarra, J., Zomaya, A.Y. (eds.) ICCS 2003, Part II. LNCS, vol. 2658, pp. 879–887. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  27. 27.
    Valmari, A.: A Stubborn Attack on State Explosion. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 156–165. Springer, Heidelberg (1991)CrossRefGoogle Scholar
  28. 28.
    van Hoesel, L., Havinga, P.: A lightweight medium access protocol (LMAC) for wireless sensor networks: Reducing preamble transmissions and transceiver state switches. In: Proc. Workshop on Networked Sensing Systems (INSS), pp. 205–208. Society of Instrument and Control Engineers, SICE (2004)Google Scholar
  29. 29.
    Zeller, A., Hildebrandt, R.: Simplifying and isolating failure-inducing input. IEEE Trans. Softw. Eng. 28, 183–200 (2002)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Matthias Woehrle
    • 1
  • Rena Bakhshi
    • 2
  • Mohammad Reza Mousavi
    • 1
    • 3
  1. 1.Embedded Software GroupDelft University of TechnologyThe Netherlands
  2. 2.Department of Computer ScienceVrije Universiteit AmsterdamThe Netherlands
  3. 3.Eindhoven University of TechnologyEindhovenThe Netherlands

Personalised recommendations