Routing Information Protocol in HOL/SPIN

1. Dimitri P. Bertsekas and Robert Gallager. Data Networks. Prentice Hall, 1991.

   Google Scholar 

2. Edmund M. Clarke and Jeannette M. Wing. Formal Methods: State of the Art and Future Directions. ACM Computing Surveys, 28(4):626–643, December 1996. report by the Working Group on Formal Methods for the ACM Workshop on Strategic Directions in Computing Research.

   Article  Google Scholar 

3. D. Cypher, D. Lee, M. Martin-Villalba, C. Prins, and D. Su. Formal Specification, Verification, and Automatic Test Generation of ATM Routing Protocol: PNNI. In Formal Description Techniques & Protocol Specification, Testing, and Verification (FORTE/PSTV) IFIP, November 1998.

   Google Scholar 

4. J.J. Garcia-Luna-Aceves and Shree Murthy. A Loop-Free Path-Finding Algorithm: Specification, Verification and Complexity. In Proceedings of IEEE INFOCOM’ 95, April 1995.

   Google Scholar 

5. M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993.

   Google Scholar 

6. Timothy G. Griffin and Gordon Wilfong. An analysis of BGP convergence properties. In Guru Parulkar and Jonathan S. Turner, editors, Proceedings of ACM SIGCOMM’ 99 Conference, pages 277–288, Boston, August 1999.

   Google Scholar 

7. Ahmed Helmy, Deborah Estrin, and Sandep Gupta. Fault-oriented Test Generation for Multicast Routing Protocol Design. In Formal Description Techniques & Protocol Specification, Testing, and Verification (FORTE/PSTV) IFIP, November 1998.

   Google Scholar 

8. C. Hendrick. Routing information protocol. RFC 1058, IETF, June 1988.

   Google Scholar 

9. Home page for the HOL interactive theorem proving system, http://www.cl.cam.ac.uk/Research/HVG/HOL.

10. Gerard J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1991.

    Google Scholar 

11. Christian Huitema. Routing in the Internet. Prentice Hall, 1995.

    Google Scholar 

12. G. Malkin. RIP Version 2 Carrying Additional Information. IETF RFC 1388, January 1993.

    Google Scholar 

13. Abdel Mokkedem, Ravi Hosabettu, Michael D. Jones, and Ganesh Gopalakrishnan. Formalization and Analysis of a Solution to the PCI 2.1 Bus Transaction Ordering Problem. Formal Methods in System Design, 16(1):93–119, January 2000.

    Article  Google Scholar 

14. Olaf Müller and Tobias Nipkow. Combining model checking and deduction for i/o-automata. In Proceedings of the Workshop on Tools and Algorithms for the Construction and Analysis of Systems, May 1995.

    Google Scholar 

15. Shree Murthy and J.J. Garcia-Luna-Aceves. An efficient routing protocol for wireless networks. ACM Mobile Netowrks and Applications Journal, October 1996. Special Issue on Routing in Mobile Communication Networks.

    Google Scholar 

16. N. Shankar. PVS: Combining specification, proof checking, and model checking. In Mandayam Srivas and Albert Camilleri, editors, Formal Methods in Computer-Aided Design (FMCAD’ 96), volume 1166 of Lecture Notes in Computer Science, pages 257–264, Palo Alto, CA, November 1996. Springer-Verlag.

    Chapter  Google Scholar 

17. Home page for the SPIN model checker. http://netlib.bell-labs.com/netlib/spin/whatispin.html.

18. Bow-Yaw Wang, José Meseguer, and Carl A. Gunter. Specification and formal verification of a PLAN algorithm in Maude. In Proceedings of the International workshop on Distributed System Valdiation and Verification, pages E:49–E:56. IEEE Computer Society Press, April 2000.

    Google Scholar 

Download references