An Integrated Approach to the Analysis of Concurrent Software Systems

该项目将研究集成两种不同但相关的方法来验证并发软件系统的可行性。具体而言，将研究与特定并发系统建模方案（称为约束表达式）相关的分析技术与用于研究并发系统同步特性的某些静态分析技术的集成。这两种方法的优点和缺点的互补性表明，它们的集成将产生超越现有分析技术的能力和实用性的技术。虽然对并发软件系统进行验证的一般方法的理论限制是相当严重的，但很少有人知道这些考虑在实践中实际上是如何限制的。由于技术的计算复杂性和缺乏自动化支持，现有并发系统分析技术的经验仅限于“玩具”系统。对可靠的并发软件的需求需要对这些技术进行更全面的试验，以确定它们如何“扩展”到有用的、实际大小的系统。

This project will investigate the feasibility of integrating two different, but related approaches to validation of concurrent software systems. Specifically, the integration of the analysis techniques that are associated with a particular concurrent system modeling scheme, called constrained expressions, and certain static analysis techniques for studying synchronization properties of concurrent systems will be studied. The complementary nature of the strengths and weaknesses of these two approaches suggests that their integration will produce techniques that surpass existing analysis techniques in both power and practical utility. While the theoretical limitation of general approaches to validation of concurrent software systems are known to be quite severe, little is known about how limiting these considerations actually are in practice. Experience with existing concurrent system analysis techniques is limited to "toy" systems, due to the computational complexity of the techniques and a lack of automated support. The demand for reliable concurrent software requires experimenting more fully with these techniques to determine how they "scale-up" to useful, realistically- sized systems.