Automated Analysis of Concurrent Systems

开发用于检测并发软件系统中的故障的自动化工具的主要障碍是状态爆炸问题：通常，并发系统的可能状态的数量与组成系统的进程的数量成指数关系。已经提出了许多技术来解决这个问题，但大多数真正的并发软件系统仍然超出了现有的分析方法的范围。该项目继续开发一种分析方法，其依据是为并发系统的某些执行的存在产生必要条件，并使用整数规划来检查这些条件的一致性。这种方法不需要枚举或显式表示正在分析的系统的状态，并且可以用于检查诸如死锁、饥饿、互斥以及事件之间的最小和最大运行时间之类的属性。这个项目包括利用并发系统的组成结构和对称性的研究，并调查与其他自动化分析方法的联系。

The major obstacle to developing automated tools for the detection of faults in concurrent software systems is the state explosion problem: the number of possible states of a concurrent system is, in general, exponential in the number of processes making up the system. A number of techniques have been proposed to address this problem, but most real concurrent software systems remain beyond the reach of existing approaches to analysis. This project continues the development of an approach to analysis based on generating necessary conditions for the existence of certain executions of a concurrent system and using integer programming to check the consistency of those conditions. This approach does not require enumeration or explicit representation of the states of the system being analyzed, and can be used to check such properties as deadlock, starvation, mutual exclusion, and minimum and maximum elapsed time between events. This project includes research to take advantage of the compositional structure and symmetries of a concurrent system and investigates connections with other automated analysis methods.