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

并发软件分析研究中的一个重要问题是在一般的理论概念和具体的实践技术之间取得平衡。这就是本研究的动因。该项目的重点是应用和调整Petri网理论来解决并发软件分析中的实用问题。所涉及的具体研究主题代表了先前努力的自然延伸点。该研究在现有实验工具包的框架内探索了Ada任务分析问题，并利用一些新的可达性概念和技术扩展了对Petri网分析的研究。其中一个重点是对各种死锁检测技术的实证研究，以及这些技术在Ada任务以外的一般语言结构中的适用性。第二个重点是研究一种广义形式的可达图及其构造。这一领域的工作利用了一些已识别的与最近使用二叉决策图(BDDS)表示符号状态空间的研究的联系。

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.