Automated Formal Verification of the DHCP Failover Protocol Using Timeout Order Abstraction

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...

Full description

Bibliographic Details
Main Authors: Umeno, Shinya (Contributor), Lynch, Nancy Ann (Contributor)
Other Authors: Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory (Contributor), Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science (Contributor)
Format: Article
Language:English
Published: Institute of Electrical and Electronics Engineers (IEEE), 2012-09-13T20:25:54Z.
Subjects:
Article
Online Access:Get fulltext

Internet

Get fulltext

Similar Items