Reasoning About Program Interactions in the Presence of Mobility

移动计算正在成为一种重要的新范式，它有可能重塑人们对分布式计算的看法。移动性对设计人员和用户对通信模式、资源可用性和应用程序行为的假设具有深远的影响。零部件从一个位置移动到另一个位置，加入或离开其附近的其他零部件组。随着应用程序的性质随着这种新的计算环境的出现而发生变化，预计将需要新的分布式算法。形式方法在这些发展中发挥着重要作用，无论是在帮助研究界更好地理解与移动计算密切相关的基本问题方面，还是在为新的设计问题提供实用解决方案方面。研究了支持上下文感知应用的自组织无线网络(AWN)。这样的网络对于危机管理、小企业的沟通和组织短暂的合作具有现实意义。AWNS有些极端的特性为研究移动计算提供了一个具有挑战性的试验台。本研究探讨现有的并发模型是否可以扩展到移动计算中，从而为移动系统的规范、设计和验证提供适当的手段。它还考虑了相关的支持系统软件，如通信协议。要做到这一点，位置的概念必须在并发性的处理中发挥更核心的作用，即使在最终目标是位置透明的情况下也是如此。本研究探讨了模块化交互的新形式。特别令人感兴趣的是在不花费开发形式证明的成本的情况下获得形式方法的优点的技术。具有所需属性的设计模式和模式只需验证一次，即可在许多应用程序中重用。***

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. ***