The objective of this project is to: Apply and adapt Petri net theory for solutions to pragmatic problems in concurrent-software analysis. Specific topics to be investigated include continued research on using Petri net techniques and tools for Ada tasking analysis and for logic specification evaluation. A number of techniques and problems will be considered including the implementation of Petri net invariant techniques and study of the relationship of this technique to the constrained expressions method.