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 |