Model checking large network protocol implementations

Abstract

Network protocols must work. The e#ects of protocol specification or implementation errors range from reduced performance, to security breaches, to bringing down entire networks. However, network protocols are di#cult 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.