Constrained Expression Analysis of 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.