Verifying Network Protocol Implementations by Symbolic Refinement Checking

Rajeev Alur and Bow-Yaw Wang

To appear at 13th Conference on Computer-Aided Verification (CAV01), Paris, France, 18-22 July 2001


Abstract

We consider the problem of establishing consistency of code implementing a network protocol with respect to the documentation as a standard RFC. The problem is formulated as a refinement checking between two models, the implementation extracted from code and the specification extracted from RFC. After simplifications based on assume-guarantee reasoning, and automatic construction of witness modules to deal with the hidden specification state, the refinement checking problem reduces to checking transition invariants. The methodology is illustrated on two case-studies involving popular network protocols, namely, PPP (point-to-point protocol for establishing connections remotely) and DHCP (dynamic-host-configuration-protocol for configuration management in mobile networks). We also present a symbolic implementation of a reduction scheme based on compressing internal transitions in a hierarchical manner, and the resulting savings for refinement checking in terms of memory size.


Server START Conference Manager
Update Time 28 Mar 2001 at 08:36:01
Maintainer www-cav01@lsv.ens-cachan.fr.
Start Conference Manager
Conference Systems