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.
