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.
CMU-CS-98-113.ps
CMU-CS-98-113Cover.ps
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 This page maintained by reports@cs.cmu.edu
School of Computer Science homepage