A Nitpick analysis of mobile IPv6

3Citations
Citations of this article
8Readers
Mendeley users who have this article in their library.

Abstract

A lightweight formal method enables partial specification and automatic analysis by sacrificing breadth of coverage and expressive power. 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 design flaw: one of the acyclicity properties does not hold. It takes only two hosts to exhibit this flaw. This paper gives self-contained overviews of Mobile IPv6 and of NP and Nitpick sufficient to understand the details of our specification and analysis.

Cite

CITATION STYLE

APA

Jackson, D., Ng, Y. C., & Wing, J. (1999). A Nitpick analysis of mobile IPv6. Formal Aspects of Computing, 11(6), 591–615. https://doi.org/10.1007/s001659970001

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free