A Nitpick Analysis of Mobile IPv6,

Abstract

A lightweight formal method enables partial specification and automatic analysis by 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 takes 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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Mar 01, 1998
Accession Number
ADA341559

Entities

People

  • Daniel Jackson
  • Jeanette M. Wing
  • Yuchung Ng

Organizations

  • Carnegie Mellon University

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Air Force
  • Case Studies
  • Computer Science
  • Computers
  • Detectors
  • Encapsulation
  • Homosexuality
  • Language
  • Network Protocols
  • Networks
  • New York
  • Software Design
  • Software Development
  • Specifications
  • Standards
  • Students

Fields of Study

  • Computer science

Readers

  • Aerial Delivery - Logistics and Supply Chain Management.
  • Computer Networking
  • Psychological Intervention/Treatment for Stress, Anxiety, PTSD, and Related Emotional and Cognitive Health Symptoms.