|
|
|
|
LEADER |
02240 am a22002293u 4500 |
001 |
72945 |
042 |
|
|
|a dc
|
100 |
1 |
0 |
|a Umeno, Shinya
|e author
|
100 |
1 |
0 |
|a Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory
|e contributor
|
100 |
1 |
0 |
|a Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science
|e contributor
|
100 |
1 |
0 |
|a Lynch, Nancy Ann
|e contributor
|
100 |
1 |
0 |
|a Umeno, Shinya
|e contributor
|
100 |
1 |
0 |
|a Lynch, Nancy Ann
|e contributor
|
700 |
1 |
0 |
|a Lynch, Nancy Ann
|e author
|
245 |
0 |
0 |
|a Automated Formal Verification of the DHCP Failover Protocol Using Timeout Order Abstraction
|
260 |
|
|
|b Institute of Electrical and Electronics Engineers (IEEE),
|c 2012-09-13T20:25:54Z.
|
856 |
|
|
|z Get fulltext
|u http://hdl.handle.net/1721.1/72945
|
520 |
|
|
|a 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.
|
520 |
|
|
|a National Science Foundation (U.S.). (Award 0702670)
|
546 |
|
|
|a en_US
|
655 |
7 |
|
|a Article
|
773 |
|
|
|t Proceedings of the 15th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS), 2010
|