Mobile computing is emerging as an important new paradigm which has the potential to reshape thinking about distributed computing. Mobility has far-reaching implications for what designers and users can assume about communication patterns, resource availability, and application behaviors. Components move from one location to another, joining or leaving groups of other components in their vicinity. New distributed algorithms are expected to be required as the nature of applications shifts with the emergence of this new kind of computing environment. Formal methods have an important role to play in the midst of these developments, both in terms of helping the research community better understand fundamental issues germane to mobile computing and in providing practical solutions to new design problems. Ad-hoc wireless networks (AWNs) supporting context-aware applications are studied in this research. Such networks have practical signifcance for crisis management, communication for small enterprises, and organization of transient collaborations. The somewhat extreme characteristics of AWNs provide a challenging testbed for studying mobile computing. This research examines whether existing models of concurrency can be extended to mobile computing and thus provide appropriate means for the specification, design and verification of mobile systems. It also considers related support system software, such as communication protocols. To accomplish this, the notion of location must play a more central role in the treatment of concurrency, even in cases where the ultimate goal is location-transparency. New forms of modular interaction are investigated in this research. Of particular interest are techniques to gain the advantages of formal methods without the costs of developing formal proofs. Design schemas and patterns with desirable properties are verified once and reused in many applications. ***
