Practical Formal Methods for the Design and Analysis of Complex Concurrent Systems

9804665该项目将为分布式系统开发一种新的编程和规范语言IOA，明确支持并行组合和抽象层次。它还将开发计算机工具来操作用IOA语言编写的程序和描述；这些工具将包括一个模拟器，现有定理证明器和模型检查器的接口，以及一个真正的代码生成器。该语言和所有工具将牢固地建立在先前开发的由输入/输出自动机组成的数学基础上。相对于外部提供的系统服务的假设，它们将使运行的系统能够被证明是正确的。这些工具将使用从高性能、容错分布式系统中选择的示例来构建和测试，特别强调组通信服务和分布式共享内存服务

9804665 This project will develop a new programming and specification language for distributed systems, IOA, with explicit support for parallel composition and levels of abstraction. It will also develop computer tools to manipulate programs and descriptions written in the IOA language; such tools will include a simulator, interfaces to existing theorem-provers and model-checkers, and a real code-generator. The language and all the tools will rest firmly upon a previously-developed mathematical foundation consisting of input/output automata. They will enable the production of running systems that are provably correct, relative to assumptions about externally-provided system services. These tools will be built and tested using examples chosen from the area of high-performance, fault-tolerant distributed systems, with particular emphasis on group communication services and distributed shared memory services."***