CAREER: Tractable Formal Methods for the Synthesis of Concurrent Programs

9702616解决了根据形式规范开发并发程序的问题。并发程序由一组相互作用的组件组成，每个组件在一台计算机上运行。正式的规范准确地说明了程序所要求的正确行为。该项目研究自动程序合成：给定正式规范，合成方法自动生成正确的程序。合成消除了手动编写程序和手动构造其正确性证明的需要。以前的合成方法有一个严重的缺点，那就是它们效率太低，只能生成最小的程序。目标是产生足够有效的合成方法来合成大型并发程序。所采用的方法是“两两分析”。以前的方法同时考虑所有的程序组件，需要分析大量的组合行为。这项研究在任何时候都只关注成对的成分，大大减少了分析负担。几乎所有大型实用程序都是并发的；它们的许多独立组件之间的交互是非常难以设计的。这项研究的意义和影响在于，它最终将提供概念性工具来帮助程序员创建这样的程序，并分析它们的行为是否符合程序规范。* * *

9702616 The problem of developing concurrent programs from formal specifications is addressed. Concurrent programs consist of a set of interacting components each running on a single computer. A formal specification states precisely the correct behavior required of the program. The project investigates automatic program synthesis: given a formal specification, the synthesis method automatically produces a correct program. Synthesis obviates the need to manually compose a program and manually construct a proof of its correctness. A serious drawback of previous synthesis methods is that they are too inefficient to generate any but the smallest programs. The objective is to produce synthesis methods sufficiently efficient to synthesize large concurrent programs. The approach taken uses "pairwise analysis." Previous approaches considered all program components simultaneously, requiring the analysis of a very large number of combined behaviors. This research looks only at pairs of components at any one time, greatly reducing the analytical burden. Almost all large, practical programs are concurrent; the interaction among their many independent components is very difficult to design properly. The significance and impact of this research is that it will eventually provide conceptual tools to help programmers create such programs and analyze whether their behavior conforms to the program specification. ***