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.
CITATION STYLE
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
Mendeley helps you to discover research relevant for your work.