Formal Methods for Reasoning About Distributed Systems

分布式系统推理的形式化方法

• 批准号: 8620027
• 负责人: Jeannette Wing
• 金额: $ 6.28万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1987
• 资助国家: 美国
• 起止时间: 1987-08-15 至 1990-01-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=8620027&HistoricalAwards=false
• 关键词: Formal; Methods; Reasoning; About; Distributed

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.

支持本地处理和分布式处理的大型计算机网络正在作为选择的计算环境而出现。 在这些环境中同时访问共享，分发以及可能复制数据的应用程序仍需要运行，但仍需要在不中断的情况下运行。 尽管分布式系统变得越来越受欢迎，但证明其可靠性却可以观察其在该领域的运营行为。 从长远来看，使用更正式的手段来证明系统属性比简单地观察使用的更具正式方法更具说服力。 该项目的目标是：（1）设计适合描述可靠分布式系统属性的规范语言； （2）开发适合推理和指导此类系统开发的证明技术。 将采用正式数学，特别是逻辑的公理和演绎方法，以定义语言和证明技术的语法和语义。 形式将通过使系统开发人员和实施者可以使语言表达丰富和证明技术的更为务实的担忧来平衡。 这项工作的结果将直接使以下社区受益：分布式系统，通过帮助人们设计，理解和理由有关可靠系统的分布式系统；通过影响未来分布式语言的设计和语义来编程语言；和正式方法，通过将公理技术扩展到尚未开发的基础。