Model Checking Large Network Protocol Implementations

9 years 5 months ago
Model Checking Large Network Protocol Implementations
Network protocols must work. The effects of protocol specification or implementation errors range from reduced performance, to security breaches, to bringing down entire networks. However, network protocols are difficult to test due to the exponential size of the state space they define. Ideally, a protocol implementation must be validated against all possible events (packet arrivals, packet losses, timeouts, etc.) in all possible protocol states. Conventional means of testing can explore only a minute fraction of these possible combinations. This paper focuses on how to effectively find errors in large network protocol implementations using model checking, a formal verification technique. Model checking involves a systematic exploration of the possible states of a system, and is well-suited to finding intricate errors lurking deep in exponential state spaces. Its primary limitation has been the effort needed to use it on software. The primary contribution of this paper are novel tech...
Madanlal Musuvathi, Dawson R. Engler
Added 31 Oct 2010
Updated 31 Oct 2010
Type Conference
Year 2004
Where NSDI
Authors Madanlal Musuvathi, Dawson R. Engler
Comments (0)