Model Checking the Time to Reach Agreement

  • Martijn Hendriks
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3829)


The timed automaton framework of Alur and Dill is a natural choice for the specification of partially synchronous distributed systems (systems which have only partial information about timing, e.g., only an upper bound on the message delay). The past has shown that verification of these systems by model checking usually is very difficult. The present paper demonstrates that an agreement algorithm of Attiya et al, which falls into a – for model checkers – particularly problematic subclass of partially synchronous distributed systems, can easily be modeled with the Uppaal model checker, and that it is possible to analyze some interesting and non-trivial instances with reasonable computational resources. Although existing techniques are used, this is an interesting case study in its own right that adds to the existing body of experience. Furthermore, the agreement algorithm has not been formally verified before to the author’s knowledge.


Model Check Computation Step Message Delivery Symmetry Reduction Synchronous System 
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.
    Lynch, N.A., Tuttle, M.R.: An introduction to Input/Output automata. CWI-Quarterly 2, 219–246 (1989)zbMATHMathSciNetGoogle Scholar
  2. 2.
    Lynch, N.A., Tuttle, M.R.: Hierarchical correctness proofs for distributed algorithms. In: PODC 1987, pp. 137–151 (1987); A full version is available as MIT Technical Report MIT/LCS/TR-387Google Scholar
  3. 3.
    Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann Publishers, San Francisco (1996)zbMATHGoogle Scholar
  4. 4.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (2000)Google Scholar
  5. 5.
    Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    Kaynar, D.K., Lynch, N.A., Segala, R., Vaandrager, F.W.: A framework for modelling timed systems with restricted hybrid automata. In: RTSS 2003, pp. 166–177. IEEE Computer Society Press, Los Alamitos (2003); A full version is available as MIT Technical Report MIT/LCS/TR-917Google Scholar
  7. 7.
    Tanenbaum, A.S.: Computer Networks. Prentice–Hall, Englewood Cliffs (1996)Google Scholar
  8. 8.
    Chkliaev, D., Hooman, J., de Vink, E.: Verification and improvement of the sliding window protocol. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 113–127. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  9. 9.
    Bodlaender, M., Guidi, J., Heerink, L.: Enhancing discovery with liveness. In: CCNC 2004. IEEE Computer Society Press, Los Alamitos (2004)Google Scholar
  10. 10.
    Katoen, J.P., Bohnenkamp, H., Klaren, R., Hermanns, H.: Embedded software analysis with MOTOR. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 268–293. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  11. 11.
    Bohnenkamp, H., Gorter, J., Guidi, J., Katoen, J.P.: Are you still there? A lightweigth algorithm to monitor node absence in self-configuring networks. In: Proceedings of DSN 2005 (2005)Google Scholar
  12. 12.
    Cheshire, S., Aboba, B., Guttman, E.: Dynamic configuration of IPv4 link-local addresses (2004),
  13. 13.
    Zhang, M., Vaandrager, F.: Analysis of a protocol for dynamic configuration of IPv4 link local addresses using Uppaal. Technical report, NIII, Radboud University Nijmegen (2005) (to appear)Google Scholar
  14. 14.
    Attiya, H., Dwork, C., Lynch, N.A., Stockmeyer, L.: Bounds on the time to reach agreement in the presence of timing uncertainty. Journal of the ACM 41, 122–152 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  15. 15.
    Lamport, L.: Real-time model checking is really simple. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 162–175. Springer, Heidelberg (2005) (to appear)CrossRefGoogle Scholar
  16. 16.
    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
  17. 17.
    Bengtsson, J., Yi, W.: Timed automata: Semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  18. 18.
    Alur, R., Courcoubetis, C., Dill, D.L.: Model checking in dense real time. Information and Computation 104, 2–34 (1993)zbMATHCrossRefMathSciNetGoogle Scholar
  19. 19.
    Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 197–212. Springer, Heidelberg (1990)Google Scholar
  20. 20.
    Hendriks, M., Behrmann, G., Larsen, K.G., Niebert, P., Vaandrager, F.W.: Adding symmetry reduction to Uppaal. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791, pp. 46–59. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  21. 21.
    Behrmann, G., Bouyer, P., Larsen, K.G., Pelańek, R.: Lower and upper bounds in zone based abstractions of timed automata. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 312–326. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  22. 22.
    Christensen, A., Kristensen, L.M., Mailund, T.: A sweep-line method for state space exploration. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 450–464. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  23. 23.
    Behrmann, G., Hune, T., Vaandrager, F.W.: Distributed timed model checking – how the search order matters. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 216–231. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  24. 24.
    Behrmann, G.: Distributed reachability analysis in timed automata. Software Tools for Technology Transfer 7, 19–30 (2005)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Martijn Hendriks
    • 1
  1. 1.Institute for Computing and Information SciencesRadboud University NijmegenNijmegenThe Netherlands

Personalised recommendations