Journal article
Modeling mobile IP in mobile UNITY
ACM transactions on software engineering and methodology, Vol.8(2), pp.115-146
04/1999
Handle:
https://hdl.handle.net/2376/100277
Abstract
With recent advances in wireless communication technology, mobile computing is an increasingly important area of research. A mobile system is one where independently executing components may migrate through some space during the course of the computation, and where the pattern of connectivity among the components changes as they move in and out of proximity. Mobile UNITY is a notation and proof logic for specifying and reasoning about mobile systems. In this article it is argued that Mobile UNITY contributes to the modular development of system specifications because of the declarative fashion in which coordination among components is specified. The packet-fowarding mechanism at the core of the Mobile IP protocol for routing to mobile hosts is taken as an example. A Mobile UNITY model of packet forwarding and the mobile system in which it must operate is developed. Proofs of correctness properties, including important real-time properties, are outlined, and the role of formal verification in the development of protocols such as Mobile IP is discussed.
Metrics
16 Record Views
Details
- Title
- Modeling mobile IP in mobile UNITY
- Creators
- Peter J McCann - Bell Labs, Naperville, ILGruia-Catalin Roman - Washington Univ., St. Louis, MO
- Publication Details
- ACM transactions on software engineering and methodology, Vol.8(2), pp.115-146
- Identifiers
- 99900546532101842
- Language
- English
- Resource Type
- Journal article