An Application of Specification-Based Design of Self-stabilization to Tracking in Wireless Sensor Networks

  • Murat Demirbas
  • Anish Arora
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5340)


In previous work, we have designed a tracking protocol, Stalk, for wireless sensor networks and proved it to be self-stabilizing at the pseudo-code (I/O automata) level. However, it is very challenging to achieve and verify self-stabilization of the same protocol at the implementation (TinyOS) level due to the size of the corresponding program at the implementation level. In this paper, we present a lightweight and practical method for specification-based design of stabilization and illustrate this method on the Stalk protocol as our case study.


Wireless Sensor Network High Level Process Implementation Level Abstract System Tracking Path 
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.
    Demirbas, M., Arora, A., Nolte, T., Lynch, N.: A hierarchy-based fault-local stabilizing algorithm for tracking in sensor networks. In: 8th International Conference on Principles of Distributed Systems (OPODIS), pp. 299–315 (2004)Google Scholar
  2. 2.
    Crossbow technology, Mica2 platform,
  3. 3.
    Gay, D., Levis, P., von Behren, R., Welsh, M., Brewer, E., Culler, D.: The nesc language: A holistic approach to networked embedded systems. In: PLDI 2003: Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, pp. 1–11 (2003)Google Scholar
  4. 4.
    Hill, J., Szewczyk, R., Woo, A., Hollar, S., Culler, D., Pister, K.: System architecture directions for network sensors. In: ASPLOS, pp. 93–104 (2000)Google Scholar
  5. 5.
    Arora, A., Demirbas, M., Kulkarni, S.S.: Graybox stabilization. In: Proceedings of the International Conference on Dependable Systems and Networks (ICDSN), pp. 389–398 (July 2001)Google Scholar
  6. 6.
    Demirbas, M., Arora, A.: Convergence refinement. In: Proceedings of the International Conference on Distributed Computing Systems (ICDCS), July 2002, pp. 589–597 (2002); Best paper(1st/335)Google Scholar
  7. 7.
    Liu, Z., Joseph, M.: Transformations of programs for fault-tolerance. Formal Aspects of Computing 4(5), 442–469 (1992)CrossRefzbMATHGoogle Scholar
  8. 8.
    Lamport, L., Merz, S.: Specifying and verifying fault-tolerant systems. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994 and ProCoS 1994, vol. 863, pp. 41–76. Springer, Heidelberg (1994)CrossRefGoogle Scholar
  9. 9.
    Dijkstra, E.W., Scholten, C.S.: Predicate Calculus and Program Semantics. Springer, Heidelberg (1990)CrossRefzbMATHGoogle Scholar
  10. 10.
    Dolev, S.: Self-Stabilization. MIT Press, Cambridge (2000)zbMATHGoogle Scholar
  11. 11.
    Demirbas, M.: Scalable design of fault-tolerance for wireless sensor networks. PhD thesis, The Ohio State University (2004)Google Scholar
  12. 12.
    Garland, S.J., Lynch, N.A.: Using i/o automata for developing distributed systems. Foundations of Component-Based Systems, 285–312 (2000)Google Scholar
  13. 13.
    Kaynar, D.K., Chefter, A., Dean, L., Garland, S., Lynch, N., Win, T.N., Ramirez, A.: The ioa simulator. Technical Report 843, MIT Laboratory for Computer Science (2002)Google Scholar
  14. 14.
    Garland, S., Guttag, J.V., Horning, J.: An overview of larch. Functional Programming, Concurrency, Simulation and Automated Reasoning (1993)Google Scholar
  15. 15.
    Tauber, J.A.: Verifiable Code Generation from Abstract I/O Automata. PhD thesis, MIT (2003)Google Scholar
  16. 16.
    Hill, J., Szewczyk, R., Woo, A., Hollar, S., Culler, D., Pister, K.: System architecture directions for network sensors. In: ASPLOS, pp. 93–104 (2000)Google Scholar
  17. 17.
    Hatcliff, J., Dwyer, M.B., Pasareanu, C.S., Robby: Foundations of the bandera abstraction tools, pp. 172–203 (2002)Google Scholar
  18. 18.
    Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Computer Aided Verification, pp. 154–169 (2000)Google Scholar
  19. 19.
    Lamport, L., Shostak, R., Pease, M.: The Byzantine generals problem. ACM Transactions on Programming Languages and Systems (1982)Google Scholar
  20. 20.
    Nesterenko, M., Arora, A.: Stabilization-preserving atomicity refinement. In: Jayanti, P. (ed.) DISC 1999. LNCS, vol. 1693, pp. 254–268. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  21. 21.
    Beauquier, J., Datta, A.K., Gradinariu, M., Magniette, F.: Self-stabilizing local mutual exclusion and daemon refinement. In: International Symposium on Distributed Computing, pp. 223–237 (2000)Google Scholar
  22. 22.
    McGuire, T.M.: Correct implementation of network protocols. PhD thesis, University at Texas at Austin (2004)Google Scholar
  23. 23.
    Leal, W.: A Foundation for Fault Tolerant Components. PhD thesis, The Ohio State University (2001)Google Scholar
  24. 24.
    Gouda, M.G., Herman, T.: Adaptive programming. IEEE Transactions on Software Engineering 17, 911–921 (1991)MathSciNetCrossRefGoogle Scholar
  25. 25.
    Leal, W., Arora, A.: Scalable self-stabilization via composition and refinement. In: Proceedings of the 24th International Conference on Distributed Computing Systems (ICDCS), IEEE, Los Alamitos (2004)Google Scholar
  26. 26.
    Arora, A., Gouda, M.G.: Distributed reset. IEEE Transactions on Computers 43(9), 1026–1038 (1994)CrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Murat Demirbas
    • 1
  • Anish Arora
    • 2
  1. 1.Computer Science & Engineering Dept.University at Buffalo, SUNYBuffaloUSA
  2. 2.Computer Science & Engineering Dept.The Ohio State UniversityColumbusUSA

Personalised recommendations