Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
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)
Crossbow technology, Mica2 platform, www.xbow.com/Products/Wireless_Sensor_Networks.htm
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)
Hill, J., Szewczyk, R., Woo, A., Hollar, S., Culler, D., Pister, K.: System architecture directions for network sensors. In: ASPLOS, pp. 93–104 (2000)
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)
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)
Liu, Z., Joseph, M.: Transformations of programs for fault-tolerance. Formal Aspects of Computing 4(5), 442–469 (1992)
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)
Dijkstra, E.W., Scholten, C.S.: Predicate Calculus and Program Semantics. Springer, Heidelberg (1990)
Dolev, S.: Self-Stabilization. MIT Press, Cambridge (2000)
Demirbas, M.: Scalable design of fault-tolerance for wireless sensor networks. PhD thesis, The Ohio State University (2004)
Garland, S.J., Lynch, N.A.: Using i/o automata for developing distributed systems. Foundations of Component-Based Systems, 285–312 (2000)
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)
Garland, S., Guttag, J.V., Horning, J.: An overview of larch. Functional Programming, Concurrency, Simulation and Automated Reasoning (1993)
Tauber, J.A.: Verifiable Code Generation from Abstract I/O Automata. PhD thesis, MIT (2003)
Hill, J., Szewczyk, R., Woo, A., Hollar, S., Culler, D., Pister, K.: System architecture directions for network sensors. In: ASPLOS, pp. 93–104 (2000)
Hatcliff, J., Dwyer, M.B., Pasareanu, C.S., Robby: Foundations of the bandera abstraction tools, pp. 172–203 (2002)
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Computer Aided Verification, pp. 154–169 (2000)
Lamport, L., Shostak, R., Pease, M.: The Byzantine generals problem. ACM Transactions on Programming Languages and Systems (1982)
Nesterenko, M., Arora, A.: Stabilization-preserving atomicity refinement. In: Jayanti, P. (ed.) DISC 1999. LNCS, vol. 1693, pp. 254–268. Springer, Heidelberg (1999)
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)
McGuire, T.M.: Correct implementation of network protocols. PhD thesis, University at Texas at Austin (2004)
Leal, W.: A Foundation for Fault Tolerant Components. PhD thesis, The Ohio State University (2001)
Gouda, M.G., Herman, T.: Adaptive programming. IEEE Transactions on Software Engineering 17, 911–921 (1991)
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)
Arora, A., Gouda, M.G.: Distributed reset. IEEE Transactions on Computers 43(9), 1026–1038 (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Demirbas, M., Arora, A. (2008). An Application of Specification-Based Design of Self-stabilization to Tracking in Wireless Sensor Networks. In: Kulkarni, S., Schiper, A. (eds) Stabilization, Safety, and Security of Distributed Systems. SSS 2008. Lecture Notes in Computer Science, vol 5340. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-89335-6_17
Download citation
DOI: https://doi.org/10.1007/978-3-540-89335-6_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-89334-9
Online ISBN: 978-3-540-89335-6
eBook Packages: Computer ScienceComputer Science (R0)