Analysis of the zeroconf protocol using UPPAAL

We report on a case study in which the model checker Uppaal is used to formally model parts of Zeroconf, a protocol for dynamic configuration of IPv4 link-local addresses that has been defined in RFC 3927 of the IETF. Our goal has been to construct a model that (a) is easy to understand by engineers, (b) comes as close as possible to the informal text (for each transition in the model there should be a corresponding piece of text in the RFC), and (c) may serve as a basis for formal verification. Our conclusion is that Uppaal, which combines extended finite state machines, C-like syntax and concepts from timed automata theory, is able to model Zeroconf in a faithful and intuitive manner, using notations that are familiar to protocol engineers. Our modeling efforts revealed several errors (or at least ambiguities) in the RFC that no one else spotted before. We also identify a number of points where Uppaal still can be improved. plying a number of abstractions, Uppaal is able to fully ex...

• Type: Conference
• Year: 2006
• Where: EMSOFT
• Authors: Biniam Gebremichael, Frits W. Vaandrager, Miaomiao Zhang
• Keywords: EMSOFT 2006, Extended Finite State, Model, Model Checker Uppaal, Software Engineering