Abstract
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.
Supported by the European Community Project IST-2001-35304 Ametist (Advanced Methods for Timed Systems), http://ametist.cs.utwente.nl/.
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.
Similar content being viewed by others
References
Lynch, N.A., Tuttle, M.R.: An introduction to Input/Output automata. CWI-Quarterly 2, 219–246 (1989)
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-387
Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann Publishers, San Francisco (1996)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (2000)
Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)
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-917
Tanenbaum, A.S.: Computer Networks. Prentice–Hall, Englewood Cliffs (1996)
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)
Bodlaender, M., Guidi, J., Heerink, L.: Enhancing discovery with liveness. In: CCNC 2004. IEEE Computer Society Press, Los Alamitos (2004)
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)
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)
Cheshire, S., Aboba, B., Guttman, E.: Dynamic configuration of IPv4 link-local addresses (2004), http://www.ietf.org/internet-drafts/draft-ietf-zeroconf-ipv4-linklocal-17.txt
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)
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)
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)
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)
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)
Alur, R., Courcoubetis, C., Dill, D.L.: Model checking in dense real time. Information and Computation 104, 2–34 (1993)
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)
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)
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)
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)
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)
Behrmann, G.: Distributed reachability analysis in timed automata. Software Tools for Technology Transfer 7, 19–30 (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hendriks, M. (2005). Model Checking the Time to Reach Agreement. In: Pettersson, P., Yi, W. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2005. Lecture Notes in Computer Science, vol 3829. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11603009_9
Download citation
DOI: https://doi.org/10.1007/11603009_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-30946-8
Online ISBN: 978-3-540-31616-9
eBook Packages: Computer ScienceComputer Science (R0)