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.