Constrained Expression Analysis of Concurrent Systems

并发系统的约束表达式分析

• 批准号: 9106645
• 负责人: George Avrunin
• 金额: $ 13.62万
• 依托单位: University of Massachusetts Amherst
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 1991
• 资助国家: 美国
• 起止时间: 1991-09-15 至 1994-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9106645&HistoricalAwards=false
• 关键词: Constrained; Expression; Analysis; Concurrent; Systems

The production and maintenance of reliable software require powerful and rigorous analysis methods. Analysis techniques for sequential systems have generally suffered from limited applicability or computational intractability. Analysis of concurrent software is even more difficult. In a previous project supported by the NSF, a toolset automating the constrained expression techniques for analyzing concurrent software systems was constructed. Experiments with that toolset have shown that it is capable of analyzing systems that approach realistic sizes for designs of concurrent systems. This project will involve efforts to extend the range of questions that the constrained expression toolset can address and to increase the size of the systems it can handle. This will involve theoretical work on the constrained expression formalism and analysis techniques and the modification of the existing toolset.

可靠软件的生产和维护需要强大而严格的分析方法。 顺序系统的分析技术通常受到适用性有限或计算困难性的困扰。 并发软件的分析更加困难。 在 NSF 支持的先前项目中，构建了一个工具集，用于自动分析并发软件系统的约束表达技术。 该工具集的实验表明，它能够分析接近并发系统设计实际尺寸的系统。 该项目将努力扩大约束表达工具集可以解决的问题范围，并扩大其可以处理的系统的规模。 这将涉及约束表达形式主义和分析技术的理论工作以及现有工具集的修改。