Advertisement

A Strategy for Automatic Verification of Stabilization of Distributed Algorithms

  • Ritwika GhoshEmail author
  • Sayan Mitra
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9039)

Abstract

Automatic verification of convergence and stabilization properties of distributed algorithms has received less attention than verification of invariance properties. We present a semi-automatic strategy for verification of stabilization properties of arbitrarily large networks under structural and fairness constraints. We introduce a sufficient condition that guarantees that every fair execution of any (arbitrarily large) instance of the system stabilizes to the target set of states. In addition to specifying the protocol executed by each agent in the network and the stabilizing set, the user also has to provide a measure function or a ranking function. With this, we show that for a restricted but useful class of distributed algorithms, the sufficient condition can be automatically checked for arbitrarily large networks, by exploiting the small model properties of these conditions. We illustrate the method by automatically verifying several well-known distributed algorithms including linkreversal, shortest path computation, distributed coloring, leader election and spanning-tree construction.

Keywords

Measure Function Model Check Transition System Interaction Graph Small Model 
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.

References

  1. 1.
    Dolev, S.: Self-stabilization. MIT Press (2000)Google Scholar
  2. 2.
    Tsitsiklis, J.N.: On the stability of asynchronous iterative processes. Mathematical Systems Theory 20(1), 137–153 (1987)CrossRefzbMATHMathSciNetGoogle Scholar
  3. 3.
    Johnson, T.T., Mitra, S.: A small model theorem for rectangular hybrid automata networks. In: Giese, H., Rosu, G. (eds.) FMOODS/FORTE 2012. LNCS, vol. 7273, pp. 18–34. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  4. 4.
    de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  5. 5.
    Dijkstra, E.W.: Self-stabilization in spite of distributed control. In: Selected Writings on Computing: A Personal Perspective, pp. 41–46. Springer (1982)Google Scholar
  6. 6.
    Theel, O.: Exploitation of ljapunov theory for verifying self-stabilizing algorithms. In: Herlihy, M. (ed.) DISC 2000. LNCS, vol. 1914, pp. 209–222. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  7. 7.
    Oehlerking, J., Dhama, A., Theel, O.: Towards automatic convergence verification of self-stabilizing algorithms. In: Tixeuil, S., Herman, T. (eds.) SSS 2005. LNCS, vol. 3764, pp. 198–213. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  8. 8.
    Theel, O.E.: A new verification technique for self-stabilizing distributed algorithms based on variable structure systems and lyapunov theory. In: HICSS (2001)Google Scholar
  9. 9.
    Dhama, A., Theel, O.: A tranformational approach for designing scheduler-oblivious self-stabilizing algorithms. In: Dolev, S., Cobb, J., Fischer, M., Yung, M. (eds.) SSS 2010. LNCS, vol. 6366, pp. 80–95. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  10. 10.
    Ghosh, S.: Distributed systems: an algorithmic approach. CRC Press (2010)Google Scholar
  11. 11.
    Umeno, S., Lynch, N.: Safety verification of an aircraft landing protocol: A refinement approach. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 557–572. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  12. 12.
    Johnson, T.T., Mitra, S.: Invariant synthesis for verification of parameterized cyber-physical systems with applications to aerospace systems. In: Proceedings of the AIAA Infotech at Aerospace Conference (AIAA Infotech 2013), Boston, MA. AIAA (August 2013)Google Scholar
  13. 13.
    Allen Emerson, E., Kahlon, V.: Reducing model checking of the many to the few. In: McAllester, D. (ed.) CADE-17. LNCS (LNAI), vol. 1831, pp. 236–254. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  14. 14.
    Duggirala, P.S., Mitra, S.: Abstraction refinement for stability. In: 2011 IEEE/ACM International Conference on Cyber-Physical Systems (ICCPS), pp. 22–31. IEEE (2011)Google Scholar
  15. 15.
    Huth, M., Ryan, M.: Logic in Computer Science: Modelling and reasoning about systems. Cambridge University Press (2004)Google Scholar
  16. 16.
    Mitra, S.: A verification framework for hybrid systems. PhD thesis, Massachusetts Institute of Technology (2007)Google Scholar
  17. 17.
    Khalil, H.K., Grizzle, J.W.: Nonlinear systems, vol. 3. Prentice Hall, Upper Saddle River (2002)zbMATHGoogle Scholar
  18. 18.
    Dershowitz, N.: Termination of rewriting. Journal of Symbolic Computation 3(1), 69–115 (1987)CrossRefzbMATHMathSciNetGoogle Scholar
  19. 19.
    Gafni, E.M., Bertsekas, D.P.: Distributed algorithms for generating loop-free routes in networks with frequently changing topology. IEEE Transactions on Communications 29(1), 11–18 (1981)CrossRefMathSciNetGoogle Scholar

Copyright information

© IFIP International Federation for Information Processing 2015

Authors and Affiliations

  1. 1.University of IllinoisUrbana ChampaignUSA

Personalised recommendations