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 demonstrate the resulting savings for refinement checking in terms of memory size.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Reference
M. Abadi and L. Lamport. The existence of refinement mappings. Theoretical Computer Science, 82(2):253–284, 1991.
M. Abadi and L. Lamport. Composing specifications. ACM TOPLAS, 15(1):73–132, 1993.
R. Alur, L. de Alfaro, R. Grosu, T. Henzinger, M. Kang, R. Majumdar, F. Mang, C. Kirsch, and B. Wang. MOCHA: A model checking tool that exploits design structure. In Proceedings of 23rd Intl. Conference on Software Engineering, 2001.
R. Alur, R. Grosu, and B.-Y. Wang. Automated refinement checking for asynchronous processes. In Proc. Third Intl. Workshop on Formal Methods in Computer-Aided Design. Springer, 2000.
R. Alur and T. Henzinger. Reactive modules. Formal Methods in System Design, 15(1):7–48, 1999.
R. Alur and B.-Y. Wang. “Next” heuristic for on-the-fly model checking. In CONCUR’99: Concurrency Theory, Tenth Intl. Conference, LNCS 1664, pages 98–113. Springer, 1999.
R. Brayton, G. Hachtel, A. Sangiovanni-Vincentelli, F. Somenzi, A. Aziz, S. Cheng, S. Edwards, S. Khatri, Y. Kukimoto, A. Pardo, S. Qadeer, R. Ranjan, S. Sarwary, T. Shiple, G. Swamy, and T. Villa. VIS: A system for verification and synthesis. In Proc. Eighth Intl. Conference on Computer Aided Verification, LNCS 1102, pages 428–432. Springer-Verlag, 1996.
J. Corbett, M. Dwyer, J. Hatcliff, S. Laubach, C. Pasareanu, Robby, and H. Zheng. Bandera: Extracting finite-state models from Java source code. In Proceedings of 22nd Intl. Conference on Software Engineering, pages 439–448. 2000.
S. Das, D. Dill, and S. Park. Experience with predicate abstraction. In Computer Aided Verification, 11th Intl. Conference, LNCS 1633, pages 160–171. Springer, 1999.
J. Fernandez, H. Garavel, A. Kerbrat, R. Mateescu, L. Mounier, and M. Sighireanu. CADP: A protocol validation and verification toolbox. In Proc. Eighth Intl. Conference on Computer-Aided Verification, LNCS 1102. Springer-Verlag, 1996.
R. Droms. Dynamic Host Configuration Protocol, March 1997. RFC 2131.
O. Grümberg and D. Long. Model checking and modular verification. ACM Transactions on Programming Languages and Systems, 16(3):843–871, 1994.
T. Henzinger, X. Liu, S. Qadeer, and S. Rajamani. Formal specification and verification of a dataflow processor array. In Proc. Intl. Conference on Computer-aided Design, pages 494–499, 1999.
T. Henzinger, S. Qadeer, and S. Rajamani. You assume, we guarantee: Methodology and case studies. In CAV 98: Computer-aided Verification, LNCS 1427, pages 521–525, 1998.
G. Holzmann. The model checker SPIN. IEEE Trans. on Software Engineering, 23(5):279–295, 1997.
G. Holzmann and M. H. Smith. Software model checking-extracting verification models from source code. In Formal Methods for Protocol Engineering and Distributed Systems, pages 481–497, Kluwer Academic Publ., 1999.
R. Kurshan. Computer-aided Verification of Coordinating Processes: the automata-theoretic approach. Princeton University Press, 1994.
N. Lynch and M. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proc. Seventh ACM Symposium on Principles of Distributed Computing, pages 137–151, 1987.
K. McMillan. A compositional rule for hardware design refinement. In CAV 97: Computer-Aided Verification, LNCS 1254, pages 24–35, 1997.
K. McMillan. Verification of an implementation of tomasulo’s algorithm by compositional model checking. In CAV 98: Computer-Aided Verification, LNCS 1427, pages 110–121, 1998.
K. Namjoshi and R. Kurshan. Syntactic program transformations for automatic abstraction. In Computer Aided Verification, 12th Intl. Conference, LNCS 1855, pages 435–449. Springer, 2000.
W. Simpson. The Point-to-Point Protocol. Computer Systems Consulting Services, July 1994. STD 51, RFC 1661.
E. Stark. A proof technique for rely-guarantee properties. In Found. of Software Technology and Theoretical Computer Science, LNCS 206, pages 369–391, 1985.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Alur, R., Wang, BY. (2001). Verifying Network Protocol Implementations by Symbolic Refinement Checking. In: Berry, G., Comon, H., Finkel, A. (eds) Computer Aided Verification. CAV 2001. Lecture Notes in Computer Science, vol 2102. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44585-4_15
Download citation
DOI: https://doi.org/10.1007/3-540-44585-4_15
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42345-4
Online ISBN: 978-3-540-44585-2
eBook Packages: Springer Book Archive