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）开发适合推理的证明技术 并指导此类系统的开发。 形式数学，特别是公理和演绎方法， 逻辑，将被用来定义语法和语义的 语言和证明技术。 正式性将由 更注重实用，使语言表达丰富， 证明技术易于系统开发人员和实现者处理。 这项工作的结果将直接有利于以下方面： 社区：分布式系统，通过帮助人们设计， 理解并推理可靠的系统;编程语言， 通过影响未来分布式的设计和语义， 语言;和形式方法，通过扩展公理技术， 尚未探索的领域。