Portal de Periódicos da CAPES

Verifying Network Protocol Implementations by Symbolic Refinement Checking

2001; Springer Science+Business Media; Linguagem: Inglês

10.1007/3-540-44585-4_15

1611-3349

Rajeev Alur, Bow-Yaw Wang,

Software Reliability and Analysis Research

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 demonstrate the resulting savings for refinement checking in terms of memory size.