Adapting Petri Net Theory and Methods to Specification and Analysis of Concurrent Software

并发软件分析研究中的一个重要问题是如何在一般理论概念和具体的实践技术之间取得平衡。 这就是本研究的动机。 该项目的重点是应用和适应Petri网理论解决并发软件分析中的实际问题。 所涉及的具体研究主题代表了以前努力的自然延伸点。 该研究探讨了Ada任务分析问题的框架内现有的实验工具包，并扩大了研究的Petri网分析使用一些新的可达性概念和技术。 一个重点领域是在各种死锁检测技术的实证研究和这些技术的适用性，以通用语言结构以外的例子Ada任务。 第二个重点是研究可达图的一种推广形式及其构造。 这一领域的工作利用了一些确定的连接到最近的研究中使用二进制决策图（BDD）的符号状态空间的表示。

One of the significant problems in concurrent-software analysis research is achieving a balance between general theoretical concepts and specific practical techniques. This is the motivation for this research. The focus of the project is on applying and adapting Petri net theory for solutions to pragmatic problems in concurrent-software analysis. The specific research topics addressed represent natural points of extension from previous efforts. The research explores Ada tasking analysis issues within the framework of an existing experimental toolkit and also expands on research in analysis of Petri nets using some new reachability concepts and techniques. One area of emphasis is in empirical studies of various deadlock detection techniques and the applicability of these techniques to generic language structures beyond the example of Ada tasking. A second emphasis is the investigation of a generalized form of reachability graph and its construction. This area of work exploits some identified connections to recent research in use of Binary-Decision Diagrams (BDDs) for representation of symbolic state spaces.