Formal Specification and Design of Mobile Systems

Gruia-Catalin Roman
Christine Julien
Qingfeng Huang

Termination detection, a classical problem in distributed computing, 
is revisited in the new setting provided by the emerging mobile 
computing technology.  A simple solution tailored for use in ad hoc 
networks is employed as a vehicle for demonstrating the applicability 
of formal requirements and design strategies to the new field of 
mobile computing.  The approach is based on well understood 
techniques in specification refinement, but the methodology is 
tailored to mobile applications and helps designers address novel 
concerns such as the mobility of hosts, transient interactions, and 
specific coordination constructs.  The proof logic and programming 
notation of Mobile UNITY provide the intellectual tools required to 
carry out this task.