Sciweavers

Share
EMSOFT
2006
Springer

Analysis of the zeroconf protocol using UPPAAL

10 years 3 months ago
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...
Biniam Gebremichael, Frits W. Vaandrager, Miaomiao
Added 22 Aug 2010
Updated 22 Aug 2010
Type Conference
Year 2006
Where EMSOFT
Authors Biniam Gebremichael, Frits W. Vaandrager, Miaomiao Zhang
Comments (0)
books