An exercise in formal reasoning about mobile communications
Amy Lynn Murphy, G.-C. Roman, George Varghese · International Workshop on Software Specification and Design · 1998
With recent advances in wireless communication and the ubiquity of laptops, mobile computing has become an important research area. An essential problem in mobile computing is the delivery of a message from a source (stationary or mobile) to a desired mobile unit. Standard solutions used in Mobile IP and cellular phones rely on tracking the mobile unit. Tracking solutions scale badly when mobile units move frequently. Our paper proposes a new message delivery algorithm and includes a proof outline using the UNITY logic. Our algorithm requires no tracking and provides stronger guarantees than existing protocols.