Computer Science Department
School of Computer Science, Carnegie Mellon University


A Nitpick Analysis of Mobile IPv6

Daniel Jackson*, Yuchung Ng**, Jeannette M. Wing

March 1998

This paper was submitted to, Formal Aspects of Computing, September 1997, and is based on work done while the first and second authors were at Carnegie Mellon University.

Keywords: Partial sepcifications, model checking, Nitpick/NP, mobile internetworking protocols, IPv6

A lightweight formal method enables partial specification and automatic analysis of sacrificing breadth of coverage and expressive power. By design, NP is a specification language that is a subset of Z and Nitpick is a tool that quickly and automatically checks properties of finite models of systems specified in NP. We used NP to state two critical acyclicity properties of Mobile IPv6, a new internetworking protocol that allows mobile hosts to communicate with each other. In our Nitpick analysis of Mobile IPv6 we discovered a flaw in a 1996 version of the design: one of the acyclicity properties does not hold. It taks only two hosts to exhibit this flaw. This paper gives self-contained overviews of Mobile IPv6 and of NP and Nitpick to understand the details of our specification and analysis. 26 pages

*MIT Laboratory for Computer Science, 545 Technology Square, Cambridge, MA 02139
**Computer Science Department, Cornell University, Ithaca, NY 14853

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by