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.
