Automated Formal Verification of the DHCP Failover Protocol Using Timeout Order Abstraction
In this paper, we present automated formal verification of the DHCP Failover protocol. We conduct bounded model-checking for the protocol using Timeout Order Abstraction (TO-Abstraction), a technique to abstract a given timed model in a certain sub-class of loosely synchronized real-time distributed...
Main Authors: | , |
---|---|
Other Authors: | , |
Format: | Article |
Language: | English |
Published: |
Institute of Electrical and Electronics Engineers (IEEE),
2012-09-13T20:25:54Z.
|
Subjects: | |
Online Access: | Get fulltext |
Summary: | In this paper, we present automated formal verification of the DHCP Failover protocol. We conduct bounded model-checking for the protocol using Timeout Order Abstraction (TO-Abstraction), a technique to abstract a given timed model in a certain sub-class of loosely synchronized real-time distributed systems into an untimed model. A resulting untimed model from TO-abstraction is a finite state machine, and therefore one can verify the model using a conventional model-checker. We have verified the protocol by bounded model-checking up to depth 20. We also experimented with "mutating" the original code to examine the efficiency of bug-finding using TO-Abstraction. We used two mutated pieces of the original code. The first one represents a model that uses a stronger failure assumption. The second one represents a model that the protocol implementer has forgot to add a certain check of a received message. We found one counterexample for each of two pieces of mutated code. In particular, the counterexample that was found for the second mutated code had a complex scenario, and we believe that it is considerably difficult to find the counterexample by human or simulations. National Science Foundation (U.S.). (Award 0702670) |
---|