CAREER: Tractable Formal Methods for the Synthesis of Concurrent Programs

职业：用于综合并发程序的易于处理的形式方法

• 批准号: 9702616
• 负责人: Paul Attie
• 金额: $ 20万
• 依托单位: Florida International University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 1997
• 资助国家: 美国
• 起止时间: 1997-05-01 至 2000-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9702616&HistoricalAwards=false
• 关键词: CAREER; Tractable; Formal; Methods; Synthesis

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. ***

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