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.
No takes yet. Share an insight, caveat, or question.
Jackson et al. (1999) studied this question.
Synapse has enriched 2 closely related papers on similar clinical questions. Consider them for comparative context: