Sciweavers

IJCSA
2006

Modeling and Formal Verification of DHCP Using SPIN

13 years 3 months ago
Modeling and Formal Verification of DHCP Using SPIN
The Dynamic Host Configuration Protocol (DHCP) is a widely used communication protocol. In this paper, a portion of the protocol is chosen for modeling and verification, namely the assignment of new IP address to a newly arriving host. PROcess Meta LAnguage (PROMELA) is used for modeling and the verification is performed using SPIN. SPIN can verify most of the communication protocols either by performing random simulations or by generating a C program. It can perform an exhaustive verification that can establish with mathematical certainty whether or not a given behavior is error-free. PROMELA is used to specify a system behavior in a formal validation model that defines interactions of processes in a distributed system and allows for the dynamic creation of concurrent processes. We have analyzed and verified various properties of the DHCP protocol such as absence of deadlock, livelock, and improper termination under various conditions such as message loss or arbitrary errors. We obta...
Syed M. S. Islam, Mohammed H. Sqalli, Sohel Khan
Added 12 Dec 2010
Updated 12 Dec 2010
Type Journal
Year 2006
Where IJCSA
Authors Syed M. S. Islam, Mohammed H. Sqalli, Sohel Khan
Comments (0)