The DHCP Failover Protocol: A Formal Perspective

Abstract. We present a formal specification and analysis of a faulttolerant DHCP algorithm, used to automatically configure certain host parameters in an IP network. Our algorithm uses ideas from an algorithm presented in [5], but is considerably simpler and at the same time more structured and rigorous. We specify the assumptions and behavior of our algorithm as traces of Timed Input/Output Automata, and prove its correctness using this formalism. Our algorithm is based on a composition of independent subalgorithms solving variants of the classical leader election and shared register problems in distributed computing. The modularity of our algorithm facilitates its understanding and analysis, and can also aid in optimizing the algorithm or proving lower bounds. Our work demonstrates that formal methods can be feasibly applied to complex real-world problems to improve and simplify their solutions.

• Type: Conference
• Year: 2007
• Where: FORTE
• Authors: Rui Fan, Ralph E. Droms, Nancy D. Griffeth, Nancy A. Lynch
• Keywords: Algorithm, Algorithm Uses Ideas, Faulttolerant Dhcp Algorithm, Formal Methods, FORTE 2007