Investigating Analysis Techniques for Concurrent Programs

本文研究的重点是并发的静态分析 软件系统。 本分析的目的是确定 给定的程序或程序规范是否满足某些 正确性要求，例如死锁的自由或没有 饥饿 本研究项目的目标是定义新的 技术和自动化工具，用于分析并发 程序. 新技术将旨在扩大和 整合现有的分析方法。 迄今为止， 并发程序的分析。 一些 方法已经实施，所产生的分析工具已经 在一些著名的并发程序例子上进行了测试。 在 然而，目前对它们的类型和大小知之甚少。 每一种方法都可以有效地应用于其中的程序， 关于该方法可以有效地 答案 一些使用线性代数或时态逻辑的方法 执行部分分析的基于技术尤其 很有希望 将对这些方法进行研究， 描述他们的相对优势和劣势。 对现有方法的评价将指导对 新的分析技术。 该地区的初步调查显示， 确定了扩展和整合的各种可能性 现有的方法。 新的分析技术必须能够适应 使用自动化分析工具。 实际 实验和性能结果的评估将发挥 在评估现有和 建议的方法。

The focus of this research is the static analysis of concurrent software systems. The purpose of this analysis is to determine whether a given program or program specification satisfies certain correctness requirements, such as freedom of deadlock or absence of starvation. The goal of this research project is to define new techniques and automated tools for the analysis of concurrent programs. The new techniques will be aimed at extending and integrating existing analysis methods. To date a number of approaches to the analysis of concurrent programs have been proposed. Some approaches have been implemented and the resulting analysis tools have been tested on some well-known examples of concurrent programs. At present, however, little is known about the types and sizes of programs to which each approach can be usefully applied, and the kinds of questions about the programs that the approach can effectively answer. Some approaches which use linear algebra or temporal logic based techniques to perform portions of the analysis are especially promising. These approaches will be investigated in an effort to characterize their relative strengths and weaknesses. The evaluation of the existing approaches will guide the definition of new analysis techniques. Preliminary investigations in this area have identified various possibilities for extending and integrating existing approaches. The new analysis techniques must be amenable to the implementation of automated analysis tools. Practical experimentations and the evaluation of performance results will play a crucial role when assessing the relative strengths of existing and proposed approaches.