A Nitpick Analysis of Mobile IPv6 |
| |
| Authors: | Daniel Jackson Yu-Chung Ng Jeannette Wing |
| |
| Affiliation: | (1) MIT Lab. for Comp. Sci. Cambridge, MA, USA, US;(2) Computer Science Dept. Cornell University, Ithaca, NY, USA, US;(3) Computer Science Dept. Carnegie Mellon University, Pittsburgh, PA, USA, US |
| |
| 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. Received September 1997 / Accepted in revised form January 2000 |
| |
| Keywords: | : Declarative specification Model checking Nitpick Z Mobile internetworking protocols |
| 本文献已被 SpringerLink 等数据库收录！ |
|
