Academic
Publications
Formal specification and analysis of zeroconf using uppaalS

Formal specification and analysis of zeroconf using uppaalS,10.1145/1952522.1952527,ACM Transactions in Embedded Computing Systems,Jasper Berendsen,Bi

Formal specification and analysis of zeroconf using uppaalS   (Citations: 2)
BibTex | RIS | RefWorks Download
The model checker Uppaal is used to formally model and analyze 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 modeling efforts revealed several errors (or at least ambiguities) in the RFC that no one else spotted before. We present two proofs of the mutual exclusion property for Zeroconf (for an arbitrary number of hosts and IP addresses): a manual, operational proof, and a proof that combines model checking with the application of a new abstraction relation that is compositional with respect to committed locations. The model checking problem has been solved using Uppaal and the abstractions have been checked by hand.
Journal: ACM Transactions in Embedded Computing Systems - TECS , vol. 10, no. 3, pp. 1-32, 2011
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
    • ...We briefly summarize the use of our compositional framework in the verification of the Zeroconf protocol for an arbitrary number of hosts [5]...
    • ...We have successfully used this approach in order to analyze Zeroconf, a protocol for dynamic configuration of IPv4 link-local addresses defined by the IETF [14,5]...

    Jasper Berendsenet al. Compositional Abstraction in Real-Time Model Checking

Sort by: