State space abstraction for parameterized self-stabilizing embedded systems

ABSTRACT

Self-stabilizing systems are systems that automatically recover from any transient fault. Proving the correctness of a parameterized self-stabilizing system, i.e., a system composed of an arbitrary number of processes, is a challenging task. For the verification of parameterized systems the method of control abstraction has been developed. However, control abstraction can only be applied to systems in which each process has a fixed number of observable variables. In this article, we propose a technique to abstract a parameterized self-stabilizing system, whose processes have a parameterized number of observable variables, to a system with fixed number of observable variables. This enables the use of control abstraction for verification. The proposed technique targets low-atomicity, shared-memory, asynchronous systems. We establish the completeness of the method under reasonable conditions and demonstrate its effectiveness by applying it on a number of self-stabilizing distributed systems.

REFERENCES

• 1: Martín Abadi , Leslie Lamport, The existence of refinement mappings, Theoretical Computer Science, v.82 n.2, p.253-284, May 31, 1991 [doi>10.1016/0304-3975(91)90224-P]
• 2: A. Arora , M. Gouda, Distributed Reset, IEEE Transactions on Computers, v.43 n.9, p.1026-1038, September 1994 [doi>10.1109/12.312126]
• 3: Arumugam, M., and Kulkarni, S. S. Self-stabilizing deterministic TDMA for sensor networks. Distributed Computing and Internet Technology (2005), 69--81.
• 4: Baukus, K., Lakhnech, Y., and Stahl, K. Verification of parameterized protocols. Journal of Universal Computer Science 7, 2 (2001), 141--158.
• 5: James E. Burns , Mohamed G. Gouda , Raymond E. Miller, Stabilization and pseudo-stabilization, Distributed Computing, v.7 n.1, p.35-42, November 1993 [doi>10.1007/BF02278854]
• 6: Clarke, E., Talupur, M., and Veith, H. Environment abstraction for parameterized verification. In VMCAI 2006: Proceedings of the 7th International Conference on Verification, Model Checking, and Abstract Interpretation (London, UK, 2006), Springer-Verlag, pp. 126--141.
• 7: Shlomi Dolev, Self-stabilization, MIT Press, Cambridge, MA, 2000
• 8: Dolev, S., and Herman, T. Superstabilizing protocols for dynamic distributed systems. Chicago Journal of Theoretical Computer Science 1997, 4 (December 1997).
• 9: E. Allen Emerson , Vineet Kahlon, Reducing Model Checking of the Many to the Few, Proceedings of the 17th International Conference on Automated Deduction, p.236-254, June 17-20, 2000
• 10: Yi Fang , Nir Piterman , Amir Pnueli , Lenore Zuck, Liveness with invisible ranking, International Journal on Software Tools for Technology Transfer (STTT), v.8 n.3, p.261-279, June 2006 [doi>10.1007/s10009-005-0193-x]
• 11: Mohamed G. Gouda , Nicholas J. Multari, Stabilizing Communication Protocols, IEEE Transactions on Computers, v.40 n.4, p.448-458, April 1991 [doi>10.1109/12.88464]
• 12: Kesten, Y., and Pnueli, A. Control and data abstraction: the cornerstones of practical formal verification. International Journal on Software Tools for Technology Transfer (STTT) 2, 4 (2000).
• 13: Verification by augmented finitary abstraction, Information and Computation, v.163 n.1, p.203-243, Nov. 25, 2000 [doi>10.1006/inco.2000.3000]
• 14: Yonit Kesten , Amir Pnueli , Elad Shahar , Lenore D. Zuck, Network Invariants in Action, Proceedings of the 13th International Conference on Concurrency Theory, p.101-115, August 20-23, 2002
• 15: Kulkarni, S. S., and Arumugam, U. Collision-free communication in sensor networks. In Self-Stabilizing Systems: 6th International Symposium, SSS 2003, San Francisco, CA, USA, June 24-25, 2003. Proceedings (2003), Springer Berlin / Heidelberg.
• 16: R. P. Kurshan , K. L. McMillan, A structural induction theorem for processes, Information and Computation, v.117 n.1, p.1-11, Feb. 15, 1995 [doi>10.1006/inco.1995.1024]
• 17: Leslie Lamport, Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2002
• 18: Nancy A. Lynch, Distributed Algorithms, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1996
• 19: Navneet Malpani , Jennifer L. Welch , Nitin Vaidya, Leader election algorithms for mobile ad hoc networks, Proceedings of the 4th international workshop on Discrete algorithms and methods for mobile computing and communications, p.96-103, August 11-11, 2000, Boston, Massachusetts, United States [doi>10.1145/345848.345871]
• 20: Amir Pnueli , Jessie Xu , Lenore D. Zuck, Liveness with (0, 1, infty)-Counter Abstraction, Proceedings of the 14th International Conference on Computer Aided Verification, p.107-122, July 27-31, 2002
• 21: Raquel S. Whittlesey-Harris , Mikhail Nesterenko, Fault-Tolerance Verification of the Fluids and Combustion Facility of the International Space Station, Proceedings of the 26th IEEE International ConferenceWorkshops on Distributed Computing Systems, p.5, July 04-07, 2006 [doi>10.1109/ICDCSW.2006.52]

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS
      C.2.4 Distributed Systems

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Reliability, Verification

Keywords:
abstraction, network invariants, parameterized systems, self-stabilizing systems, verification