Formal Methods for Reasoning About Distributed Systems

支持本地和分布式处理的大型计算机网络正在成为首选的计算环境。在这些环境中并发访问共享、分布式和可能复制的数据的应用程序需要在系统发生故障时不中断地运行。尽管分布式系统正变得越来越流行，但要证明它们的可靠性，还需要观察它们在现场的操作行为。比起简单地观察系统的使用，使用更正式的方法来展示系统的特性会更有说服力，从长远来看也更经济有效。该项目的目标是：(1)设计适合描述可靠分布式系统属性的规范语言；(2)开发适合于推理和指导此类系统开发的证明技术。形式数学，特别是逻辑的公理化和演绎方法，将被用来定义语言和证明技术的语法和语义。正式性将被更加实用的关注所平衡，即使语言表达丰富，证明技术易于系统开发人员和实现者处理。这项工作的结果将直接使以下社区受益：分布式系统，通过帮助人们设计、理解和推理可靠的系统；编程语言，通过影响未来分布式语言的设计和语义；形式方法，通过将公理技术扩展到尚未探索的领域。

Large networks of computers supporting both local and distributed processing are emerging as the computing environments of choice. Application programs, which concurrently access shared, distributed, and possibly replicated data in these environments, need to run without interruption despite failures occurring in the system. Although distributed systems are becoming more popular, demonstrating their reliability is left up to observing their operational behavior in the field. It would be more convincing, and in the long run more cost- effective, to use a more formal means of demonstrating a system's properties than by simply observing it in use. The objectives of this project are: (1) to design specification languages suitable for describing properties of reliable distributed systems; and (2) to develop proof techniques suitable for reasoning about and guiding the development of such systems. Formal mathematics, in particular axiomatic and deductive methods of logic, will be employed to define the syntax and semantics of the languages and proof techniques. Formality will be balanced by the more pragmatic concerns of making the language expressively rich and proof techniques tractable by system developers and implementors. The results of this work will directly benefit the following communities: distributed systems, by helping people design, understand, and reason about reliable systems; programming languages, by influencing the design and semantics of future distributed languages; and formal methods, by extending axiomatic techniques to as yet unexplored grounds.