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: | 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: | |
Online Access: | Get fulltext |
Similar Items
-
Timeout Order Abstraction for Time-Parametric Verification of Loosely Synchronized Real-Time Distributed Systems
by: Umeno, Shinya, et al.
Published: (2011) -
DHCP Hierarchical Failover (DHCP-HF) Servers over a VPN Interconnected Campus
by: Lucas Trombeta, et al.
Published: (2019-03-01) -
Replication and Abstraction: Symmetry in Automated Formal Verification
by: Thomas Wahl, et al.
Published: (2010-04-01) -
The pain of the timeout
by: Robbins RA
Published: (2011-06-01) -
Distributed DHCP for WMNs using IPv6
by: Molerón Bermudez, Daniel, et al.
Published: (2007)